/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-11-07 11:28 +0100 24287 AList.thy
-rw-r--r-- 2014-11-07 11:28 +0100 2357 AList_Mapping.thy
-rw-r--r-- 2014-11-07 11:28 +0100 365 BNF_Axiomatization.thy
-rw-r--r-- 2014-11-07 11:28 +0100 29016 BigO.thy
-rw-r--r-- 2014-11-07 11:28 +0100 4386 Bit.thy
-rw-r--r-- 2014-11-07 11:28 +0100 11396 Boolean_Algebra.thy
-rw-r--r-- 2014-11-07 11:28 +0100 784 Cardinal_Notations.thy
-rw-r--r-- 2014-11-07 11:28 +0100 20983 Cardinality.thy
-rw-r--r-- 2014-11-07 11:28 +0100 3820 Char_ord.thy
-rw-r--r-- 2014-11-07 11:28 +0100 3680 Code_Abstract_Nat.thy
-rw-r--r-- 2014-11-07 11:28 +0100 4767 Code_Binary_Nat.thy
-rw-r--r-- 2014-11-07 11:28 +0100 4444 Code_Char.thy
-rw-r--r-- 2014-11-07 11:28 +0100 458 Code_Prolog.thy
-rw-r--r-- 2014-11-07 11:28 +0100 5839 Code_Real_Approx_By_Float.thy
-rw-r--r-- 2014-11-07 11:28 +0100 2803 Code_Target_Int.thy
-rw-r--r-- 2014-11-07 11:28 +0100 3945 Code_Target_Nat.thy
-rw-r--r-- 2014-11-07 11:28 +0100 270 Code_Target_Numeral.thy
-rw-r--r-- 2014-11-07 11:28 +0100 5669 Code_Test.thy
-rw-r--r-- 2014-11-07 11:28 +0100 5100 ContNotDenum.thy
-rw-r--r-- 2014-11-07 11:28 +0100 31625 Convex.thy
-rw-r--r-- 2014-11-07 11:28 +0100 10347 Countable.thy
-rw-r--r-- 2014-11-07 11:28 +0100 14298 Countable_Set.thy
-rw-r--r-- 2014-11-07 11:28 +0100 7305 Countable_Set_Type.thy
-rw-r--r-- 2014-11-07 11:28 +0100 6370 DAList.thy
-rw-r--r-- 2014-11-07 11:28 +0100 15570 DAList_Multiset.thy
-rw-r--r-- 2014-11-07 11:28 +0100 1167 Debug.thy
-rw-r--r-- 2014-11-07 11:28 +0100 4008 Diagonal_Subsequence.thy
-rw-r--r-- 2014-11-07 11:28 +0100 5948 Discrete.thy
-rw-r--r-- 2014-11-07 11:28 +0100 5868 Dlist.thy
-rw-r--r-- 2014-11-07 11:28 +0100 5175 Extended.thy
-rw-r--r-- 2014-11-07 11:28 +0100 20772 Extended_Nat.thy
-rw-r--r-- 2014-11-07 11:28 +0100 84495 Extended_Real.thy
-rw-r--r-- 2014-11-07 11:28 +0100 44855 FSet.thy
-rw-r--r-- 2014-11-07 11:28 +0100 71386 FinFun.thy
-rw-r--r-- 2014-11-07 11:28 +0100 630 FinFun_Syntax.thy
-rw-r--r-- 2014-11-07 11:28 +0100 9874 Finite_Lattice.thy
-rw-r--r-- 2014-11-07 11:28 +0100 67132 Float.thy
-rw-r--r-- 2014-11-07 11:28 +0100 137935 Formal_Power_Series.thy
-rw-r--r-- 2014-11-07 11:28 +0100 18292 Fraction_Field.thy
-rw-r--r-- 2014-11-07 11:28 +0100 3512 Fun_Lexorder.thy
-rw-r--r-- 2014-11-07 11:28 +0100 24282 FuncSet.thy
-rw-r--r-- 2014-11-07 11:28 +0100 5680 Function_Algebras.thy
-rw-r--r-- 2014-11-07 11:28 +0100 1676 Function_Division.thy
-rw-r--r-- 2014-11-07 11:28 +0100 15157 Function_Growth.thy
-rw-r--r-- 2014-11-07 11:28 +0100 44860 Fundamental_Theorem_Algebra.thy
-rw-r--r-- 2014-11-07 11:28 +0100 12940 Groups_Big_Fun.thy
-rw-r--r-- 2014-11-07 11:28 +0100 4006 IArray.thy
-rw-r--r-- 2014-11-07 11:28 +0100 7035 Indicator_Function.thy
-rw-r--r-- 2014-11-07 11:28 +0100 18146 Infinite_Set.thy
-rw-r--r-- 2014-11-07 11:28 +0100 13040 Inner_Product.thy
-rw-r--r-- 2014-11-07 11:28 +0100 3774 LaTeXsugar.thy
-rw-r--r-- 2014-11-07 11:28 +0100 19360 Lattice_Algebras.thy
-rw-r--r-- 2014-11-07 11:28 +0100 11564 Lattice_Constructions.thy
-rw-r--r-- 2014-11-07 11:28 +0100 828 Lattice_Syntax.thy
-rw-r--r-- 2014-11-07 11:28 +0100 1109 Library.thy
-rw-r--r-- 2014-11-07 11:28 +0100 12586 Liminf_Limsup.thy
-rw-r--r-- 2014-11-07 11:28 +0100 13158 Linear_Temporal_Logic_on_Streams.thy
-rw-r--r-- 2014-11-07 11:28 +0100 4074 ListVector.thy
-rw-r--r-- 2014-11-07 11:28 +0100 3325 List_lexord.thy
-rw-r--r-- 2014-11-07 11:28 +0100 10072 Lub_Glb.thy
-rw-r--r-- 2014-11-07 11:28 +0100 14200 Mapping.thy
-rw-r--r-- 2014-11-07 11:28 +0100 2271 Monad_Syntax.thy
-rw-r--r-- 2014-11-07 11:28 +0100 12315 More_List.thy
-rw-r--r-- 2014-11-07 11:28 +0100 86782 Multiset.thy
-rw-r--r-- 2014-11-07 11:28 +0100 11858 Nat_Bijection.thy
-rw-r--r-- 2014-11-07 11:28 +0100 4243 NthRoot_Limits.thy
-rw-r--r-- 2014-11-07 11:28 +0100 17069 Numeral_Type.thy
-rw-r--r-- 2014-11-07 11:28 +0100 14773 Old_Datatype.thy
-rw-r--r-- 2014-11-07 11:28 +0100 2322 Old_Recdef.thy
-rw-r--r-- 2014-11-07 11:28 +0100 14181 Old_SMT.thy
-rw-r--r-- 2014-11-07 11:28 +0100 12766 Option_ord.thy
-rw-r--r-- 2014-11-07 11:28 +0100 2098 OptionalSugar.thy
-rw-r--r-- 2014-11-07 11:28 +0100 5065 Order_Continuity.thy
-rw-r--r-- 2014-11-07 11:28 +0100 1591 Parallel.thy
-rw-r--r-- 2014-11-07 11:28 +0100 8542 Permutation.thy
-rw-r--r-- 2014-11-07 11:28 +0100 35114 Permutations.thy
-rw-r--r-- 2014-11-07 11:28 +0100 1158 Phantom_Type.thy
-rw-r--r-- 2014-11-07 11:28 +0100 10789 Poly_Deriv.thy
-rw-r--r-- 2014-11-07 11:28 +0100 58132 Polynomial.thy
-rw-r--r-- 2014-11-07 11:28 +0100 7685 Predicate_Compile_Alternative_Defs.thy
-rw-r--r-- 2014-11-07 11:28 +0100 280 Predicate_Compile_Quickcheck.thy
-rw-r--r-- 2014-11-07 11:28 +0100 1695 Prefix_Order.thy
-rw-r--r-- 2014-11-07 11:28 +0100 1874 Preorder.thy
-rw-r--r-- 2014-11-07 11:28 +0100 3326 Product_Lexorder.thy
-rw-r--r-- 2014-11-07 11:28 +0100 6424 Product_Order.thy
-rw-r--r-- 2014-11-07 11:28 +0100 21771 Product_Vector.thy
-rw-r--r-- 2014-11-07 11:28 +0100 3091 Product_plus.thy
-rw-r--r-- 2014-11-07 11:28 +0100 6909 Quotient_List.thy
-rw-r--r-- 2014-11-07 11:28 +0100 2464 Quotient_Option.thy
-rw-r--r-- 2014-11-07 11:28 +0100 3661 Quotient_Product.thy
-rw-r--r-- 2014-11-07 11:28 +0100 3610 Quotient_Set.thy
-rw-r--r-- 2014-11-07 11:28 +0100 2903 Quotient_Sum.thy
-rw-r--r-- 2014-11-07 11:28 +0100 309 Quotient_Syntax.thy
-rw-r--r-- 2014-11-07 11:28 +0100 6515 Quotient_Type.thy
-rw-r--r-- 2014-11-07 11:28 +0100 6557 RBT.thy
-rw-r--r-- 2014-11-07 11:28 +0100 96823 RBT_Impl.thy
-rw-r--r-- 2014-11-07 11:28 +0100 5688 RBT_Mapping.thy
-rw-r--r-- 2014-11-07 11:28 +0100 29181 RBT_Set.thy
-rw-r--r-- 2014-11-07 11:28 +0100 2666 README.html
-rw-r--r-- 2014-11-07 11:28 +0100 17386 Ramsey.thy
-rw-r--r-- 2014-11-07 11:28 +0100 1103 Reflection.thy
-rw-r--r-- 2014-11-07 11:28 +0100 6505 Refute.thy
-rw-r--r-- 2014-11-07 11:28 +0100 7271 Saturated.thy
-rw-r--r-- 2014-11-07 11:28 +0100 13423 Set_Algebras.thy
-rw-r--r-- 2014-11-07 11:28 +0100 240 Simps_Case_Conv.thy
-rw-r--r-- 2014-11-07 11:28 +0100 5290 State_Monad.thy
-rw-r--r-- 2014-11-07 11:28 +0100 20891 Stream.thy
-rw-r--r-- 2014-11-07 11:28 +0100 25804 Sublist.thy
-rw-r--r-- 2014-11-07 11:28 +0100 2901 Sublist_Order.thy
-rw-r--r-- 2014-11-07 11:28 +0100 526 Sum_of_Squares.thy
-rw-r--r-- 2014-11-07 11:28 +0100 1148 Sum_of_Squares_Remote.thy
-rw-r--r-- 2014-11-07 11:28 +0100 6674 Transitive_Closure_Table.thy
-rw-r--r-- 2014-11-07 11:28 +0100 4346 Tree.thy
-rw-r--r-- 2014-11-07 11:28 +0100 15169 While_Combinator.thy
-rw-r--r-- 2014-11-07 11:28 +0100 5462 bnf_axiomatization.ML
-rw-r--r-- 2014-11-07 11:28 +0100 7615 bnf_lfp_countable.ML
-rw-r--r-- 2014-11-07 11:28 +0100 21246 code_test.ML
-rw-r--r-- 2014-11-07 11:28 +0100 33000 positivstellensatz.ML
-rw-r--r-- 2014-11-07 11:28 +0100 145225 refute.ML
-rw-r--r-- 2014-11-07 11:28 +0100 7741 simps_case_conv.ML