Session HOL-Real_Asymp

Theories

• HOL-Library.BNF_Corec
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML›
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec.ML›
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML›
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML›
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML›
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML›
• HOL-Library.Landau_Symbols
• Lazy_Eval
  • File ‹lazy_eval.ML›
• Inst_Existentials
  • File ‹inst_existentials.ML›
• Eventuallize
• Multiseries_Expansion
  • File ‹asymptotic_basis.ML›
  • File ‹exp_log_expression.ML›
  • File ‹expansion_interface.ML›
  • File ‹multiseries_expansion.ML›
  • File ‹real_asymp.ML›
• Multiseries_Expansion_Bounds
  • File ‹multiseries_expansion_bounds.ML›
• Real_Asymp
  • File ‹real_asymp_diag.ML›
• HOL-Library.Lattice_Algebras
• HOL-Library.Set_Algebras
• HOL-Library.Interval
• HOL-Library.Log_Nat
• HOL-Library.Float
• HOL-Library.Interval_Float
• HOL-Decision_Procs.Dense_Linear_Order
  • File ‹langford_data.ML›
  • File ‹ferrante_rackoff_data.ML›
  • File ‹langford.ML›
  • File ‹ferrante_rackoff.ML›
• HOL-Decision_Procs.Approximation_Bounds
• HOL-Library.Code_Target_Int
• HOL-Library.Code_Abstract_Nat
• HOL-Library.Code_Target_Nat
• HOL-Library.Code_Target_Numeral
• HOL-Library.Code_Target_Numeral_Float
• HOL-Decision_Procs.Approximation
  • File ‹approximation.ML›
  • File ‹approximation_generator.ML›
• Real_Asymp_Approx
• Real_Asymp_Examples