Session HOL-Decision_Procs

Theories

• Conversions
• Algebra_Aux
• Commutative_Ring
• Cooper
  • File ‹cooper_tac.ML›
• Dense_Linear_Order
  • File ‹langford_data.ML›
  • File ‹ferrante_rackoff_data.ML›
  • File ‹langford.ML›
  • File ‹ferrante_rackoff.ML›
• DP_Library
• Ferrack
  • File ‹ferrack_tac.ML›
• HOL-Library.Old_Recdef
  • File ‹old_recdef.ML›
• MIR
  • File ‹mir_tac.ML›
• HOL-Library.Lattice_Algebras
• HOL-Library.Set_Algebras
• HOL-Library.Interval
• HOL-Library.Log_Nat
• HOL-Library.Float
• HOL-Library.Interval_Float
• Approximation_Bounds
• HOL-Library.Code_Target_Numeral_Float
• Approximation
  • File ‹approximation.ML›
  • File ‹approximation_generator.ML›
• Rat_Pair
• Polynomial_List
• Reflected_Multivariate_Polynomial
• Parametric_Ferrante_Rackoff
• Commutative_Ring_Complete
• Reflective_Field
• Commutative_Ring_Ex
• Approximation_Ex
• Approximation_Quickcheck_Ex
• Dense_Linear_Order_Ex
• Decision_Procs