/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-10-29 17:01 +0100 24286 AList.thy
-rw-r--r-- 2014-10-29 17:01 +0100 2356 AList_Mapping.thy
-rw-r--r-- 2014-10-29 17:01 +0100 364 BNF_Axiomatization.thy
-rw-r--r-- 2014-10-29 17:01 +0100 29015 BigO.thy
-rw-r--r-- 2014-10-29 17:01 +0100 4385 Bit.thy
-rw-r--r-- 2014-10-29 17:01 +0100 11395 Boolean_Algebra.thy
-rw-r--r-- 2014-10-29 17:01 +0100 783 Cardinal_Notations.thy
-rw-r--r-- 2014-10-29 17:01 +0100 20982 Cardinality.thy
-rw-r--r-- 2014-10-29 17:01 +0100 3819 Char_ord.thy
-rw-r--r-- 2014-10-29 17:01 +0100 3679 Code_Abstract_Nat.thy
-rw-r--r-- 2014-10-29 17:01 +0100 4766 Code_Binary_Nat.thy
-rw-r--r-- 2014-10-29 17:01 +0100 4443 Code_Char.thy
-rw-r--r-- 2014-10-29 17:01 +0100 457 Code_Prolog.thy
-rw-r--r-- 2014-10-29 17:01 +0100 5839 Code_Real_Approx_By_Float.thy
-rw-r--r-- 2014-10-29 17:01 +0100 2802 Code_Target_Int.thy
-rw-r--r-- 2014-10-29 17:01 +0100 3944 Code_Target_Nat.thy
-rw-r--r-- 2014-10-29 17:01 +0100 269 Code_Target_Numeral.thy
-rw-r--r-- 2014-10-29 17:01 +0100 5669 Code_Test.thy
-rw-r--r-- 2014-10-29 17:01 +0100 5099 ContNotDenum.thy
-rw-r--r-- 2014-10-29 17:01 +0100 31624 Convex.thy
-rw-r--r-- 2014-10-29 17:01 +0100 10346 Countable.thy
-rw-r--r-- 2014-10-29 17:01 +0100 14297 Countable_Set.thy
-rw-r--r-- 2014-10-29 17:01 +0100 7304 Countable_Set_Type.thy
-rw-r--r-- 2014-10-29 17:01 +0100 6369 DAList.thy
-rw-r--r-- 2014-10-29 17:01 +0100 15569 DAList_Multiset.thy
-rw-r--r-- 2014-10-29 17:01 +0100 1166 Debug.thy
-rw-r--r-- 2014-10-29 17:01 +0100 4007 Diagonal_Subsequence.thy
-rw-r--r-- 2014-10-29 17:01 +0100 5947 Discrete.thy
-rw-r--r-- 2014-10-29 17:01 +0100 5867 Dlist.thy
-rw-r--r-- 2014-10-29 17:01 +0100 5175 Extended.thy
-rw-r--r-- 2014-10-29 17:01 +0100 20771 Extended_Nat.thy
-rw-r--r-- 2014-10-29 17:01 +0100 84494 Extended_Real.thy
-rw-r--r-- 2014-10-29 17:01 +0100 44854 FSet.thy
-rw-r--r-- 2014-10-29 17:01 +0100 71385 FinFun.thy
-rw-r--r-- 2014-10-29 17:01 +0100 629 FinFun_Syntax.thy
-rw-r--r-- 2014-10-29 17:01 +0100 9874 Finite_Lattice.thy
-rw-r--r-- 2014-10-29 17:01 +0100 67160 Float.thy
-rw-r--r-- 2014-10-29 17:01 +0100 137934 Formal_Power_Series.thy
-rw-r--r-- 2014-10-29 17:01 +0100 18291 Fraction_Field.thy
-rw-r--r-- 2014-10-29 17:01 +0100 3511 Fun_Lexorder.thy
-rw-r--r-- 2014-10-29 17:01 +0100 24281 FuncSet.thy
-rw-r--r-- 2014-10-29 17:01 +0100 5679 Function_Algebras.thy
-rw-r--r-- 2014-10-29 17:01 +0100 1675 Function_Division.thy
-rw-r--r-- 2014-10-29 17:01 +0100 15156 Function_Growth.thy
-rw-r--r-- 2014-10-29 17:01 +0100 44859 Fundamental_Theorem_Algebra.thy
-rw-r--r-- 2014-10-29 17:01 +0100 12939 Groups_Big_Fun.thy
-rw-r--r-- 2014-10-29 17:01 +0100 4005 IArray.thy
-rw-r--r-- 2014-10-29 17:01 +0100 7034 Indicator_Function.thy
-rw-r--r-- 2014-10-29 17:01 +0100 18145 Infinite_Set.thy
-rw-r--r-- 2014-10-29 17:01 +0100 13039 Inner_Product.thy
-rw-r--r-- 2014-10-29 17:01 +0100 3774 LaTeXsugar.thy
-rw-r--r-- 2014-10-29 17:01 +0100 19359 Lattice_Algebras.thy
-rw-r--r-- 2014-10-29 17:01 +0100 11564 Lattice_Constructions.thy
-rw-r--r-- 2014-10-29 17:01 +0100 827 Lattice_Syntax.thy
-rw-r--r-- 2014-10-29 17:01 +0100 1109 Library.thy
-rw-r--r-- 2014-10-29 17:01 +0100 12585 Liminf_Limsup.thy
-rw-r--r-- 2014-10-29 17:01 +0100 13157 Linear_Temporal_Logic_on_Streams.thy
-rw-r--r-- 2014-10-29 17:01 +0100 4073 ListVector.thy
-rw-r--r-- 2014-10-29 17:01 +0100 3324 List_lexord.thy
-rw-r--r-- 2014-10-29 17:01 +0100 10071 Lub_Glb.thy
-rw-r--r-- 2014-10-29 17:01 +0100 14199 Mapping.thy
-rw-r--r-- 2014-10-29 17:01 +0100 2270 Monad_Syntax.thy
-rw-r--r-- 2014-10-29 17:01 +0100 12314 More_List.thy
-rw-r--r-- 2014-10-29 17:01 +0100 86781 Multiset.thy
-rw-r--r-- 2014-10-29 17:01 +0100 11816 Nat_Bijection.thy
-rw-r--r-- 2014-10-29 17:01 +0100 4243 NthRoot_Limits.thy
-rw-r--r-- 2014-10-29 17:01 +0100 17068 Numeral_Type.thy
-rw-r--r-- 2014-10-29 17:01 +0100 14772 Old_Datatype.thy
-rw-r--r-- 2014-10-29 17:01 +0100 2321 Old_Recdef.thy
-rw-r--r-- 2014-10-29 17:01 +0100 14180 Old_SMT.thy
-rw-r--r-- 2014-10-29 17:01 +0100 12765 Option_ord.thy
-rw-r--r-- 2014-10-29 17:01 +0100 2098 OptionalSugar.thy
-rw-r--r-- 2014-10-29 17:01 +0100 5064 Order_Continuity.thy
-rw-r--r-- 2014-10-29 17:01 +0100 1590 Parallel.thy
-rw-r--r-- 2014-10-29 17:01 +0100 8541 Permutation.thy
-rw-r--r-- 2014-10-29 17:01 +0100 35113 Permutations.thy
-rw-r--r-- 2014-10-29 17:01 +0100 1157 Phantom_Type.thy
-rw-r--r-- 2014-10-29 17:01 +0100 10788 Poly_Deriv.thy
-rw-r--r-- 2014-10-29 17:01 +0100 58131 Polynomial.thy
-rw-r--r-- 2014-10-29 17:01 +0100 7685 Predicate_Compile_Alternative_Defs.thy
-rw-r--r-- 2014-10-29 17:01 +0100 279 Predicate_Compile_Quickcheck.thy
-rw-r--r-- 2014-10-29 17:01 +0100 1694 Prefix_Order.thy
-rw-r--r-- 2014-10-29 17:01 +0100 1873 Preorder.thy
-rw-r--r-- 2014-10-29 17:01 +0100 3325 Product_Lexorder.thy
-rw-r--r-- 2014-10-29 17:01 +0100 6423 Product_Order.thy
-rw-r--r-- 2014-10-29 17:01 +0100 21770 Product_Vector.thy
-rw-r--r-- 2014-10-29 17:01 +0100 3090 Product_plus.thy
-rw-r--r-- 2014-10-29 17:01 +0100 6908 Quotient_List.thy
-rw-r--r-- 2014-10-29 17:01 +0100 2445 Quotient_Option.thy
-rw-r--r-- 2014-10-29 17:01 +0100 3660 Quotient_Product.thy
-rw-r--r-- 2014-10-29 17:01 +0100 3609 Quotient_Set.thy
-rw-r--r-- 2014-10-29 17:01 +0100 2955 Quotient_Sum.thy
-rw-r--r-- 2014-10-29 17:01 +0100 308 Quotient_Syntax.thy
-rw-r--r-- 2014-10-29 17:01 +0100 6514 Quotient_Type.thy
-rw-r--r-- 2014-10-29 17:01 +0100 6556 RBT.thy
-rw-r--r-- 2014-10-29 17:01 +0100 96822 RBT_Impl.thy
-rw-r--r-- 2014-10-29 17:01 +0100 5687 RBT_Mapping.thy
-rw-r--r-- 2014-10-29 17:01 +0100 29180 RBT_Set.thy
-rw-r--r-- 2014-10-29 17:01 +0100 2666 README.html
-rw-r--r-- 2014-10-29 17:01 +0100 17385 Ramsey.thy
-rw-r--r-- 2014-10-29 17:01 +0100 1102 Reflection.thy
-rw-r--r-- 2014-10-29 17:01 +0100 6504 Refute.thy
-rw-r--r-- 2014-10-29 17:01 +0100 7270 Saturated.thy
-rw-r--r-- 2014-10-29 17:01 +0100 13422 Set_Algebras.thy
-rw-r--r-- 2014-10-29 17:01 +0100 240 Simps_Case_Conv.thy
-rw-r--r-- 2014-10-29 17:01 +0100 5289 State_Monad.thy
-rw-r--r-- 2014-10-29 17:01 +0100 20890 Stream.thy
-rw-r--r-- 2014-10-29 17:01 +0100 25803 Sublist.thy
-rw-r--r-- 2014-10-29 17:01 +0100 2900 Sublist_Order.thy
-rw-r--r-- 2014-10-29 17:01 +0100 525 Sum_of_Squares.thy
-rw-r--r-- 2014-10-29 17:01 +0100 1147 Sum_of_Squares_Remote.thy
-rw-r--r-- 2014-10-29 17:01 +0100 6673 Transitive_Closure_Table.thy
-rw-r--r-- 2014-10-29 17:01 +0100 4345 Tree.thy
-rw-r--r-- 2014-10-29 17:01 +0100 15168 While_Combinator.thy
-rw-r--r-- 2014-10-29 17:01 +0100 5469 bnf_axiomatization.ML
-rw-r--r-- 2014-10-29 17:01 +0100 7615 bnf_lfp_countable.ML
-rw-r--r-- 2014-10-29 17:01 +0100 21174 code_test.ML
-rw-r--r-- 2014-10-29 17:01 +0100 33000 positivstellensatz.ML
-rw-r--r-- 2014-10-29 17:01 +0100 145374 refute.ML
-rw-r--r-- 2014-10-29 17:01 +0100 7741 simps_case_conv.ML