Session Physical_Quantities
View
theory dependencies
View
document
View
outline
Theories
Power_int
HOL-Library.Phantom_Type
HOL-Library.Cardinality
HOL-Library.Code_Cardinality
Enum_extra
Groups_mult
HOL-Eisbach.Eisbach
File ‹parse_tools.ML›
File ‹method_closure.ML›
File ‹eisbach_rule_insts.ML›
File ‹match_method.ML›
ISQ_Dimensions
ISQ_Quantities
ISQ_Proof
ISQ_Algebra
ISQ_Units
ISQ_Conversion
ISQ
SI_Units
CGS
SI_Constants
SI_Prefix
SI_Derived
SI_Accepted
SI_Imperial
SI
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›
SI_Astronomical
SI_Pretty
BIS