Session Irrationality_J_Hancl

Theories

• HOL-Library.Lattice_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›
• Irrationality_J_Hancl