Session Affine_Arithmetic
View
theory dependencies
View
document
View
outline
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›
HOL-Library.Adhoc_Overloading
File ‹adhoc_overloading.ML›
HOL-Library.Monad_Syntax
HOL-Library.AList
HOL-Library.Mapping
List-Index.List_Index
HOL-Library.Code_Cardinality
Affine_Arithmetic_Auxiliarities
Executable_Euclidean_Space
HOL-Combinatorics.List_Permutation
Affine_Form
Floatarith_Expression
Deriving.Generator_Aux
File ‹bnf_access.ML›
File ‹generator_aux.ML›
Deriving.Derive_Manager
File ‹derive_manager.ML›
Deriving.Comparator
Deriving.Comparator_Generator
File ‹comparator_generator.ML›
Deriving.Compare
File ‹compare_code.ML›
Deriving.Compare_Generator
File ‹compare_generator.ML›
HOL-Library.Char_ord
Deriving.Compare_Instances
Deriving.Equality_Generator
File ‹equality_generator.ML›
Deriving.Equality_Instances
HOL-Library.Type_Length
HOL-Library.Word
File ‹Tools/word_lib.ML›
File ‹Tools/smt_word.ML›
Word_Lib.More_Arithmetic
Word_Lib.More_Divides
Word_Lib.More_Bit_Ring
Word_Lib.More_Word
Word_Lib.Bit_Shifts_Infix_Syntax
Word_Lib.Most_significant_bit
Word_Lib.Least_significant_bit
Word_Lib.Generic_set_bit
Word_Lib.Bit_Comprehension
HOL-Library.Signed_Division
Word_Lib.Signed_Division_Word
Native_Word.Code_Target_Word_Base
Native_Word.Word_Type_Copies
Native_Word.Code_Int_Integer_Conversion
Native_Word.Code_Target_Integer_Bit
Native_Word.Uint32
Collections.HashCode
Deriving.Hash_Generator
File ‹hash_generator.ML›
Deriving.Hash_Instances
Deriving.Countable_Generator
Deriving.Derive
HOL-Library.RBT_Impl
HOL-Library.RBT
HOL-Library.RBT_Mapping
Straight_Line_Program
Affine_Approximation
Counterclockwise
Counterclockwise_Vector
Counterclockwise_2D_Strict
Polygon
Counterclockwise_2D_Arbitrary
Intersection
Affine_Code
Show.Show
File ‹show_generator.ML›
Show.Show_Instances
Optimize_Integer
Optimize_Float
Print
Float_Real
Ex_Affine_Approximation
Ex_Ineqs
Ex_Inter
Affine_Arithmetic