/src/HOL/Library/
drwxr-xr-x [up]
drwxr-xr-x Old_SMT
drwxr-xr-x Sum_of_Squares
drwxr-xr-x document
-rw-r--r-- 2014-09-21 16:56 +0200 24286 AList.thy
-rw-r--r-- 2014-09-21 16:56 +0200 2356 AList_Mapping.thy
-rw-r--r-- 2014-09-21 16:56 +0200 364 BNF_Axiomatization.thy
-rw-r--r-- 2014-09-21 16:56 +0200 29012 BigO.thy
-rw-r--r-- 2014-09-21 16:56 +0200 4385 Bit.thy
-rw-r--r-- 2014-09-21 16:56 +0200 11395 Boolean_Algebra.thy
-rw-r--r-- 2014-09-21 16:56 +0200 783 Cardinal_Notations.thy
-rw-r--r-- 2014-09-21 16:56 +0200 20982 Cardinality.thy
-rw-r--r-- 2014-09-21 16:56 +0200 3819 Char_ord.thy
-rw-r--r-- 2014-09-21 16:56 +0200 3679 Code_Abstract_Nat.thy
-rw-r--r-- 2014-09-21 16:56 +0200 4766 Code_Binary_Nat.thy
-rw-r--r-- 2014-09-21 16:56 +0200 4443 Code_Char.thy
-rw-r--r-- 2014-09-21 16:56 +0200 457 Code_Prolog.thy
-rw-r--r-- 2014-09-21 16:56 +0200 5839 Code_Real_Approx_By_Float.thy
-rw-r--r-- 2014-09-21 16:56 +0200 2802 Code_Target_Int.thy
-rw-r--r-- 2014-09-21 16:56 +0200 3944 Code_Target_Nat.thy
-rw-r--r-- 2014-09-21 16:56 +0200 269 Code_Target_Numeral.thy
-rw-r--r-- 2014-09-21 16:56 +0200 5099 ContNotDenum.thy
-rw-r--r-- 2014-09-21 16:56 +0200 31624 Convex.thy
-rw-r--r-- 2014-09-21 16:56 +0200 10346 Countable.thy
-rw-r--r-- 2014-09-21 16:56 +0200 14297 Countable_Set.thy
-rw-r--r-- 2014-09-21 16:56 +0200 7304 Countable_Set_Type.thy
-rw-r--r-- 2014-09-21 16:56 +0200 5701 DAList.thy
-rw-r--r-- 2014-09-21 16:56 +0200 14902 DAList_Multiset.thy
-rw-r--r-- 2014-09-21 16:56 +0200 1166 Debug.thy
-rw-r--r-- 2014-09-21 16:56 +0200 4007 Diagonal_Subsequence.thy
-rw-r--r-- 2014-09-21 16:56 +0200 5796 Discrete.thy
-rw-r--r-- 2014-09-21 16:56 +0200 5867 Dlist.thy
-rw-r--r-- 2014-09-21 16:56 +0200 5175 Extended.thy
-rw-r--r-- 2014-09-21 16:56 +0200 20771 Extended_Nat.thy
-rw-r--r-- 2014-09-21 16:56 +0200 84537 Extended_Real.thy
-rw-r--r-- 2014-09-21 16:56 +0200 44854 FSet.thy
-rw-r--r-- 2014-09-21 16:56 +0200 71429 FinFun.thy
-rw-r--r-- 2014-09-21 16:56 +0200 629 FinFun_Syntax.thy
-rw-r--r-- 2014-09-21 16:56 +0200 9874 Finite_Lattice.thy
-rw-r--r-- 2014-09-21 16:56 +0200 67160 Float.thy
-rw-r--r-- 2014-09-21 16:56 +0200 138041 Formal_Power_Series.thy
-rw-r--r-- 2014-09-21 16:56 +0200 18291 Fraction_Field.thy
-rw-r--r-- 2014-09-21 16:56 +0200 3511 Fun_Lexorder.thy
-rw-r--r-- 2014-09-21 16:56 +0200 22136 FuncSet.thy
-rw-r--r-- 2014-09-21 16:56 +0200 5679 Function_Algebras.thy
-rw-r--r-- 2014-09-21 16:56 +0200 1675 Function_Division.thy
-rw-r--r-- 2014-09-21 16:56 +0200 15156 Function_Growth.thy
-rw-r--r-- 2014-09-21 16:56 +0200 44859 Fundamental_Theorem_Algebra.thy
-rw-r--r-- 2014-09-21 16:56 +0200 12383 Groups_Big_Fun.thy
-rw-r--r-- 2014-09-21 16:56 +0200 4005 IArray.thy
-rw-r--r-- 2014-09-21 16:56 +0200 7104 Indicator_Function.thy
-rw-r--r-- 2014-09-21 16:56 +0200 18145 Infinite_Set.thy
-rw-r--r-- 2014-09-21 16:56 +0200 13039 Inner_Product.thy
-rw-r--r-- 2014-09-21 16:56 +0200 3774 LaTeXsugar.thy
-rw-r--r-- 2014-09-21 16:56 +0200 19359 Lattice_Algebras.thy
-rw-r--r-- 2014-09-21 16:56 +0200 11564 Lattice_Constructions.thy
-rw-r--r-- 2014-09-21 16:56 +0200 827 Lattice_Syntax.thy
-rw-r--r-- 2014-09-21 16:56 +0200 1055 Library.thy
-rw-r--r-- 2014-09-21 16:56 +0200 12585 Liminf_Limsup.thy
-rw-r--r-- 2014-09-21 16:56 +0200 4073 ListVector.thy
-rw-r--r-- 2014-09-21 16:56 +0200 3324 List_lexord.thy
-rw-r--r-- 2014-09-21 16:56 +0200 10075 Lubs_Glbs.thy
-rw-r--r-- 2014-09-21 16:56 +0200 14199 Mapping.thy
-rw-r--r-- 2014-09-21 16:56 +0200 2270 Monad_Syntax.thy
-rw-r--r-- 2014-09-21 16:56 +0200 9438 More_List.thy
-rw-r--r-- 2014-09-21 16:56 +0200 87410 Multiset.thy
-rw-r--r-- 2014-09-21 16:56 +0200 12099 Nat_Bijection.thy
-rw-r--r-- 2014-09-21 16:56 +0200 4243 NthRoot_Limits.thy
-rw-r--r-- 2014-09-21 16:56 +0200 17068 Numeral_Type.thy
-rw-r--r-- 2014-09-21 16:56 +0200 14772 Old_Datatype.thy
-rw-r--r-- 2014-09-21 16:56 +0200 2339 Old_Recdef.thy
-rw-r--r-- 2014-09-21 16:56 +0200 14231 Old_SMT.thy
-rw-r--r-- 2014-09-21 16:56 +0200 12765 Option_ord.thy
-rw-r--r-- 2014-09-21 16:56 +0200 2098 OptionalSugar.thy
-rw-r--r-- 2014-09-21 16:56 +0200 5064 Order_Continuity.thy
-rw-r--r-- 2014-09-21 16:56 +0200 1590 Parallel.thy
-rw-r--r-- 2014-09-21 16:56 +0200 8541 Permutation.thy
-rw-r--r-- 2014-09-21 16:56 +0200 35120 Permutations.thy
-rw-r--r-- 2014-09-21 16:56 +0200 1157 Phantom_Type.thy
-rw-r--r-- 2014-09-21 16:56 +0200 10788 Poly_Deriv.thy
-rw-r--r-- 2014-09-21 16:56 +0200 57953 Polynomial.thy
-rw-r--r-- 2014-09-21 16:56 +0200 7685 Predicate_Compile_Alternative_Defs.thy
-rw-r--r-- 2014-09-21 16:56 +0200 327 Predicate_Compile_Quickcheck.thy
-rw-r--r-- 2014-09-21 16:56 +0200 1694 Prefix_Order.thy
-rw-r--r-- 2014-09-21 16:56 +0200 1873 Preorder.thy
-rw-r--r-- 2014-09-21 16:56 +0200 3325 Product_Lexorder.thy
-rw-r--r-- 2014-09-21 16:56 +0200 6423 Product_Order.thy
-rw-r--r-- 2014-09-21 16:56 +0200 21770 Product_Vector.thy
-rw-r--r-- 2014-09-21 16:56 +0200 3090 Product_plus.thy
-rw-r--r-- 2014-09-21 16:56 +0200 6908 Quotient_List.thy
-rw-r--r-- 2014-09-21 16:56 +0200 2445 Quotient_Option.thy
-rw-r--r-- 2014-09-21 16:56 +0200 3660 Quotient_Product.thy
-rw-r--r-- 2014-09-21 16:56 +0200 3609 Quotient_Set.thy
-rw-r--r-- 2014-09-21 16:56 +0200 2955 Quotient_Sum.thy
-rw-r--r-- 2014-09-21 16:56 +0200 308 Quotient_Syntax.thy
-rw-r--r-- 2014-09-21 16:56 +0200 6514 Quotient_Type.thy
-rw-r--r-- 2014-09-21 16:56 +0200 6556 RBT.thy
-rw-r--r-- 2014-09-21 16:56 +0200 96822 RBT_Impl.thy
-rw-r--r-- 2014-09-21 16:56 +0200 5687 RBT_Mapping.thy
-rw-r--r-- 2014-09-21 16:56 +0200 29180 RBT_Set.thy
-rw-r--r-- 2014-09-21 16:56 +0200 2666 README.html
-rw-r--r-- 2014-09-21 16:56 +0200 17382 Ramsey.thy
-rw-r--r-- 2014-09-21 16:56 +0200 1102 Reflection.thy
-rw-r--r-- 2014-09-21 16:56 +0200 6523 Refute.thy
-rw-r--r-- 2014-09-21 16:56 +0200 7270 Saturated.thy
-rw-r--r-- 2014-09-21 16:56 +0200 13422 Set_Algebras.thy
-rw-r--r-- 2014-09-21 16:56 +0200 240 Simps_Case_Conv.thy
-rw-r--r-- 2014-09-21 16:56 +0200 5289 State_Monad.thy
-rw-r--r-- 2014-09-21 16:56 +0200 25803 Sublist.thy
-rw-r--r-- 2014-09-21 16:56 +0200 2900 Sublist_Order.thy
-rw-r--r-- 2014-09-21 16:56 +0200 11859 Sum_of_Squares.thy
-rw-r--r-- 2014-09-21 16:56 +0200 1147 Sum_of_Squares_Remote.thy
-rw-r--r-- 2014-09-21 16:56 +0200 6673 Transitive_Closure_Table.thy
-rw-r--r-- 2014-09-21 16:56 +0200 4069 Tree.thy
-rw-r--r-- 2014-09-21 16:56 +0200 15168 While_Combinator.thy
-rw-r--r-- 2014-09-21 16:56 +0200 5350 bnf_axiomatization.ML
-rw-r--r-- 2014-09-21 16:56 +0200 7503 bnf_lfp_countable.ML
-rw-r--r-- 2014-09-21 16:56 +0200 32806 positivstellensatz.ML
-rw-r--r-- 2014-09-21 16:56 +0200 145696 refute.ML
-rw-r--r-- 2014-09-21 16:56 +0200 7741 simps_case_conv.ML