/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-- 2015-06-07 12:43 +0200 27630 AList.thy
-rw-r--r-- 2015-06-07 12:43 +0200 2356 AList_Mapping.thy
-rw-r--r-- 2015-06-07 12:43 +0200 365 BNF_Axiomatization.thy
-rw-r--r-- 2015-06-07 12:43 +0200 28893 BigO.thy
-rw-r--r-- 2015-06-07 12:43 +0200 4377 Bit.thy
-rw-r--r-- 2015-06-07 12:43 +0200 11396 Boolean_Algebra.thy
-rw-r--r-- 2015-06-07 12:43 +0200 784 Cardinal_Notations.thy
-rw-r--r-- 2015-06-07 12:43 +0200 20983 Cardinality.thy
-rw-r--r-- 2015-06-07 12:43 +0200 3820 Char_ord.thy
-rw-r--r-- 2015-06-07 12:43 +0200 3662 Code_Abstract_Nat.thy
-rw-r--r-- 2015-06-07 12:43 +0200 4767 Code_Binary_Nat.thy
-rw-r--r-- 2015-06-07 12:43 +0200 4444 Code_Char.thy
-rw-r--r-- 2015-06-07 12:43 +0200 458 Code_Prolog.thy
-rw-r--r-- 2015-06-07 12:43 +0200 5844 Code_Real_Approx_By_Float.thy
-rw-r--r-- 2015-06-07 12:43 +0200 2803 Code_Target_Int.thy
-rw-r--r-- 2015-06-07 12:43 +0200 3945 Code_Target_Nat.thy
-rw-r--r-- 2015-06-07 12:43 +0200 270 Code_Target_Numeral.thy
-rw-r--r-- 2015-06-07 12:43 +0200 5692 Code_Test.thy
-rw-r--r-- 2015-06-07 12:43 +0200 5825 ContNotDenum.thy
-rw-r--r-- 2015-06-07 12:43 +0200 31997 Convex.thy
-rw-r--r-- 2015-06-07 12:43 +0200 10304 Countable.thy
-rw-r--r-- 2015-06-07 12:43 +0200 15060 Countable_Set.thy
-rw-r--r-- 2015-06-07 12:43 +0200 29742 Countable_Set_Type.thy
-rw-r--r-- 2015-06-07 12:43 +0200 8277 DAList.thy
-rw-r--r-- 2015-06-07 12:43 +0200 15557 DAList_Multiset.thy
-rw-r--r-- 2015-06-07 12:43 +0200 1167 Debug.thy
-rw-r--r-- 2015-06-07 12:43 +0200 4008 Diagonal_Subsequence.thy
-rw-r--r-- 2015-06-07 12:43 +0200 5938 Discrete.thy
-rw-r--r-- 2015-06-07 12:43 +0200 5868 Dlist.thy
-rw-r--r-- 2015-06-07 12:43 +0200 5175 Extended.thy
-rw-r--r-- 2015-06-07 12:43 +0200 21062 Extended_Nat.thy
-rw-r--r-- 2015-06-07 12:43 +0200 99406 Extended_Real.thy
-rw-r--r-- 2015-06-07 12:43 +0200 44896 FSet.thy
-rw-r--r-- 2015-06-07 12:43 +0200 71386 FinFun.thy
-rw-r--r-- 2015-06-07 12:43 +0200 630 FinFun_Syntax.thy
-rw-r--r-- 2015-06-07 12:43 +0200 9874 Finite_Lattice.thy
-rw-r--r-- 2015-06-07 12:43 +0200 86879 Float.thy
-rw-r--r-- 2015-06-07 12:43 +0200 136316 Formal_Power_Series.thy
-rw-r--r-- 2015-06-07 12:43 +0200 18285 Fraction_Field.thy
-rw-r--r-- 2015-06-07 12:43 +0200 3512 Fun_Lexorder.thy
-rw-r--r-- 2015-06-07 12:43 +0200 24535 FuncSet.thy
-rw-r--r-- 2015-06-07 12:43 +0200 5715 Function_Algebras.thy
-rw-r--r-- 2015-06-07 12:43 +0200 1678 Function_Division.thy
-rw-r--r-- 2015-06-07 12:43 +0200 15160 Function_Growth.thy
-rw-r--r-- 2015-06-07 12:43 +0200 44830 Fundamental_Theorem_Algebra.thy
-rw-r--r-- 2015-06-07 12:43 +0200 12940 Groups_Big_Fun.thy
-rw-r--r-- 2015-06-07 12:43 +0200 4301 IArray.thy
-rw-r--r-- 2015-06-07 12:43 +0200 7187 Indicator_Function.thy
-rw-r--r-- 2015-06-07 12:43 +0200 16028 Infinite_Set.thy
-rw-r--r-- 2015-06-07 12:43 +0200 13040 Inner_Product.thy
-rw-r--r-- 2015-06-07 12:43 +0200 3774 LaTeXsugar.thy
-rw-r--r-- 2015-06-07 12:43 +0200 19360 Lattice_Algebras.thy
-rw-r--r-- 2015-06-07 12:43 +0200 11564 Lattice_Constructions.thy
-rw-r--r-- 2015-06-07 12:43 +0200 828 Lattice_Syntax.thy
-rw-r--r-- 2015-06-07 12:43 +0200 1132 Library.thy
-rw-r--r-- 2015-06-07 12:43 +0200 12586 Liminf_Limsup.thy
-rw-r--r-- 2015-06-07 12:43 +0200 28479 Linear_Temporal_Logic_on_Streams.thy
-rw-r--r-- 2015-06-07 12:43 +0200 4074 ListVector.thy
-rw-r--r-- 2015-06-07 12:43 +0200 3325 List_lexord.thy
-rw-r--r-- 2015-06-07 12:43 +0200 10072 Lub_Glb.thy
-rw-r--r-- 2015-06-07 12:43 +0200 14333 Mapping.thy
-rw-r--r-- 2015-06-07 12:43 +0200 2273 Monad_Syntax.thy
-rw-r--r-- 2015-06-07 12:43 +0200 12315 More_List.thy
-rw-r--r-- 2015-06-07 12:43 +0200 90646 Multiset.thy
-rw-r--r-- 2015-06-07 12:43 +0200 13749 Multiset_Order.thy
-rw-r--r-- 2015-06-07 12:43 +0200 12241 Nat_Bijection.thy
-rw-r--r-- 2015-06-07 12:43 +0200 17069 Numeral_Type.thy
-rw-r--r-- 2015-06-07 12:43 +0200 14773 Old_Datatype.thy
-rw-r--r-- 2015-06-07 12:43 +0200 2322 Old_Recdef.thy
-rw-r--r-- 2015-06-07 12:43 +0200 14187 Old_SMT.thy
-rw-r--r-- 2015-06-07 12:43 +0200 12766 Option_ord.thy
-rw-r--r-- 2015-06-07 12:43 +0200 2098 OptionalSugar.thy
-rw-r--r-- 2015-06-07 12:43 +0200 5379 Order_Continuity.thy
-rw-r--r-- 2015-06-07 12:43 +0200 1591 Parallel.thy
-rw-r--r-- 2015-06-07 12:43 +0200 8542 Permutation.thy
-rw-r--r-- 2015-06-07 12:43 +0200 34828 Permutations.thy
-rw-r--r-- 2015-06-07 12:43 +0200 1158 Phantom_Type.thy
-rw-r--r-- 2015-06-07 12:43 +0200 10789 Poly_Deriv.thy
-rw-r--r-- 2015-06-07 12:43 +0200 56980 Polynomial.thy
-rw-r--r-- 2015-06-07 12:43 +0200 7860 Predicate_Compile_Alternative_Defs.thy
-rw-r--r-- 2015-06-07 12:43 +0200 280 Predicate_Compile_Quickcheck.thy
-rw-r--r-- 2015-06-07 12:43 +0200 1695 Prefix_Order.thy
-rw-r--r-- 2015-06-07 12:43 +0200 1874 Preorder.thy
-rw-r--r-- 2015-06-07 12:43 +0200 3326 Product_Lexorder.thy
-rw-r--r-- 2015-06-07 12:43 +0200 6424 Product_Order.thy
-rw-r--r-- 2015-06-07 12:43 +0200 21887 Product_Vector.thy
-rw-r--r-- 2015-06-07 12:43 +0200 3108 Product_plus.thy
-rw-r--r-- 2015-06-07 12:43 +0200 6568 Quadratic_Discriminant.thy
-rw-r--r-- 2015-06-07 12:43 +0200 6913 Quotient_List.thy
-rw-r--r-- 2015-06-07 12:43 +0200 2464 Quotient_Option.thy
-rw-r--r-- 2015-06-07 12:43 +0200 3661 Quotient_Product.thy
-rw-r--r-- 2015-06-07 12:43 +0200 3610 Quotient_Set.thy
-rw-r--r-- 2015-06-07 12:43 +0200 2903 Quotient_Sum.thy
-rw-r--r-- 2015-06-07 12:43 +0200 309 Quotient_Syntax.thy
-rw-r--r-- 2015-06-07 12:43 +0200 6885 Quotient_Type.thy
-rw-r--r-- 2015-06-07 12:43 +0200 6557 RBT.thy
-rw-r--r-- 2015-06-07 12:43 +0200 96560 RBT_Impl.thy
-rw-r--r-- 2015-06-07 12:43 +0200 5676 RBT_Mapping.thy
-rw-r--r-- 2015-06-07 12:43 +0200 29181 RBT_Set.thy
-rw-r--r-- 2015-06-07 12:43 +0200 2666 README.html
-rw-r--r-- 2015-06-07 12:43 +0200 17386 Ramsey.thy
-rw-r--r-- 2015-06-07 12:43 +0200 1107 Reflection.thy
-rw-r--r-- 2015-06-07 12:43 +0200 6505 Refute.thy
-rw-r--r-- 2015-06-07 12:43 +0200 1237 Rewrite.thy
-rw-r--r-- 2015-06-07 12:43 +0200 7271 Saturated.thy
-rw-r--r-- 2015-06-07 12:43 +0200 13423 Set_Algebras.thy
-rw-r--r-- 2015-06-07 12:43 +0200 240 Simps_Case_Conv.thy
-rw-r--r-- 2015-06-07 12:43 +0200 5290 State_Monad.thy
-rw-r--r-- 2015-06-07 12:43 +0200 21868 Stream.thy
-rw-r--r-- 2015-06-07 12:43 +0200 25797 Sublist.thy
-rw-r--r-- 2015-06-07 12:43 +0200 2901 Sublist_Order.thy
-rw-r--r-- 2015-06-07 12:43 +0200 526 Sum_of_Squares.thy
-rw-r--r-- 2015-06-07 12:43 +0200 1148 Sum_of_Squares_Remote.thy
-rw-r--r-- 2015-06-07 12:43 +0200 6674 Transitive_Closure_Table.thy
-rw-r--r-- 2015-06-07 12:43 +0200 6927 Tree.thy
-rw-r--r-- 2015-06-07 12:43 +0200 1351 Tree_Multiset.thy
-rw-r--r-- 2015-06-07 12:43 +0200 15169 While_Combinator.thy
-rw-r--r-- 2015-06-07 12:43 +0200 5463 bnf_axiomatization.ML
-rw-r--r-- 2015-06-07 12:43 +0200 7637 bnf_lfp_countable.ML
-rw-r--r-- 2015-06-07 12:43 +0200 8457 cconv.ML
-rw-r--r-- 2015-06-07 12:43 +0200 21222 code_test.ML
-rw-r--r-- 2015-06-07 12:43 +0200 33083 positivstellensatz.ML
-rw-r--r-- 2015-06-07 12:43 +0200 145257 refute.ML
-rw-r--r-- 2015-06-07 12:43 +0200 17063 rewrite.ML
-rw-r--r-- 2015-06-07 12:43 +0200 7905 simps_case_conv.ML