introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
(*<*)
theory Library
imports
AList
BigO
Bit
BNF_Decl
Boolean_Algebra
Char_ord
ContNotDenum
Convex
Countable
Countable_Set_Type
Debug
Diagonal_Subsequence
Dlist
Extended
Extended_Nat
Extended_Real
FinFun
Float
Formal_Power_Series
Fraction_Field
FSet
FuncSet
Function_Division
Function_Growth
Fundamental_Theorem_Algebra
Indicator_Function
Infinite_Set
Inner_Product
IArray
Lattice_Algebras
Lattice_Syntax
ListVector
Kleene_Algebra
Mapping
Monad_Syntax
Multiset
Numeral_Type
OptionalSugar
Option_ord
Order_Continuity
Parallel
Permutation
Permutations
Poly_Deriv
Polynomial
Preorder
Product_Vector
Quotient_List
Quotient_Option
Quotient_Product
Quotient_Set
Quotient_Sum
Quotient_Syntax
Quotient_Type
Ramsey
Reflection
Saturated
Set_Algebras
State_Monad
Sublist
Sum_of_Squares
Transitive_Closure_Table
While_Combinator
begin
end
(*>*)