Session HOL-Library
View
theory dependencies
View
README
View
document
View
outline
Theories
AList
Function_Algebras
Set_Algebras
BigO
Bit
BNF_Axiomatization
BNF_Corec
Boolean_Algebra
While_Combinator
Bourbaki_Witt_Fixpoint
Char_ord
Code_Test
Lattice_Syntax
Combine_PER
Complete_Partial_Order2
Old_Datatype
Nat_Bijection
Countable
Infinite_Set
Countable_Set
Countable_Complete_Lattices
Cardinal_Notations
Countable_Set_Type
Debug
Diagonal_Subsequence
Disjoint_Sets
Dlist
Simps_Case_Conv
Extended
Order_Continuity
Extended_Nat
Liminf_Limsup
Extended_Real
Indicator_Function
Extended_Nonnegative_Real
FSet
Finite_Map
Log_Nat
Lattice_Algebras
Float
FuncSet
Function_Division
Preorder
Discrete
Function_Growth
Fun_Lexorder
Going_To_Filter
Groups_Big_Fun
IArray
Lattice_Constructions
Stream
Sublist
Linear_Temporal_Logic_on_Streams
ListVector
Lub_Glb
Mapping
Adhoc_Overloading
Monad_Syntax
More_List
Cancellation
Multiset
Multiset_Order
Permutations
Multiset_Permutations
Nonpos_Ints
Phantom_Type
Cardinality
Numeral_Type
Omega_Words_Fun
Open_State_Syntax
Option_ord
Parallel
Pattern_Aliases
Periodic_Fun
Perm
Permutation
Product_Plus
Quadratic_Discriminant
Quotient_Syntax
Quotient_Set
Quotient_Product
Quotient_Option
Quotient_List
Quotient_Sum
Quotient_Type
Ramsey
Reflection
Rewrite
Type_Length
Saturated
State_Monad
Stirling
Sum_of_Squares
Transitive_Closure_Table
Tree
Tree_Multiset
Tree_Real
Uprod
Library
Product_Order
Finite_Lattice
List_lexord
Prefix_Order
Product_Lexorder
Subseq_Order
AList_Mapping
Code_Abstract_Nat
Code_Binary_Nat
Code_Char
Code_Prolog
Code_Target_Int
Code_Real_Approx_By_Float
Code_Target_Nat
Code_Target_Numeral
DAList
DAList_Multiset
RBT_Impl
RBT
RBT_Mapping
RBT_Set
LaTeXsugar
OptionalSugar
Predicate_Compile_Alternative_Defs
Predicate_Compile_Quickcheck
Old_Recdef
Refute