/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-07-18 20:47 +0200 27762 AList.thy
-rw-r--r-- 2015-07-18 20:47 +0200 2365 AList_Mapping.thy
-rw-r--r-- 2015-07-18 20:47 +0200 374 BNF_Axiomatization.thy
-rw-r--r-- 2015-07-18 20:47 +0200 28949 BigO.thy
-rw-r--r-- 2015-07-18 20:47 +0200 4439 Bit.thy
-rw-r--r-- 2015-07-18 20:47 +0200 11450 Boolean_Algebra.thy
-rw-r--r-- 2015-07-18 20:47 +0200 793 Cardinal_Notations.thy
-rw-r--r-- 2015-07-18 20:47 +0200 21303 Cardinality.thy
-rw-r--r-- 2015-07-18 20:47 +0200 3834 Char_ord.thy
-rw-r--r-- 2015-07-18 20:47 +0200 3744 Code_Abstract_Nat.thy
-rw-r--r-- 2015-07-18 20:47 +0200 4823 Code_Binary_Nat.thy
-rw-r--r-- 2015-07-18 20:47 +0200 4473 Code_Char.thy
-rw-r--r-- 2015-07-18 20:47 +0200 494 Code_Prolog.thy
-rw-r--r-- 2015-07-18 20:47 +0200 5853 Code_Real_Approx_By_Float.thy
-rw-r--r-- 2015-07-18 20:47 +0200 2812 Code_Target_Int.thy
-rw-r--r-- 2015-07-18 20:47 +0200 3972 Code_Target_Nat.thy
-rw-r--r-- 2015-07-18 20:47 +0200 279 Code_Target_Numeral.thy
-rw-r--r-- 2015-07-18 20:47 +0200 5759 Code_Test.thy
-rw-r--r-- 2015-07-18 20:47 +0200 5918 ContNotDenum.thy
-rw-r--r-- 2015-07-18 20:47 +0200 32689 Convex.thy
-rw-r--r-- 2015-07-18 20:47 +0200 10543 Countable.thy
-rw-r--r-- 2015-07-18 20:47 +0200 15192 Countable_Set.thy
-rw-r--r-- 2015-07-18 20:47 +0200 29914 Countable_Set_Type.thy
-rw-r--r-- 2015-07-18 20:47 +0200 8278 DAList.thy
-rw-r--r-- 2015-07-18 20:47 +0200 15576 DAList_Multiset.thy
-rw-r--r-- 2015-07-18 20:47 +0200 1185 Debug.thy
-rw-r--r-- 2015-07-18 20:47 +0200 4017 Diagonal_Subsequence.thy
-rw-r--r-- 2015-07-18 20:47 +0200 6030 Discrete.thy
-rw-r--r-- 2015-07-18 20:47 +0200 6560 Disjoint_Sets.thy
-rw-r--r-- 2015-07-18 20:47 +0200 5982 Dlist.thy
-rw-r--r-- 2015-07-18 20:47 +0200 5193 Extended.thy
-rw-r--r-- 2015-07-18 20:47 +0200 21920 Extended_Nat.thy
-rw-r--r-- 2015-07-18 20:47 +0200 102907 Extended_Real.thy
-rw-r--r-- 2015-07-18 20:47 +0200 47710 FSet.thy
-rw-r--r-- 2015-07-18 20:47 +0200 72059 FinFun.thy
-rw-r--r-- 2015-07-18 20:47 +0200 639 FinFun_Syntax.thy
-rw-r--r-- 2015-07-18 20:47 +0200 10013 Finite_Lattice.thy
-rw-r--r-- 2015-07-18 20:47 +0200 89173 Float.thy
-rw-r--r-- 2015-07-18 20:47 +0200 135925 Formal_Power_Series.thy
-rw-r--r-- 2015-07-18 20:47 +0200 18365 Fraction_Field.thy
-rw-r--r-- 2015-07-18 20:47 +0200 3551 Fun_Lexorder.thy
-rw-r--r-- 2015-07-18 20:47 +0200 24535 FuncSet.thy
-rw-r--r-- 2015-07-18 20:47 +0200 5847 Function_Algebras.thy
-rw-r--r-- 2015-07-18 20:47 +0200 1724 Function_Division.thy
-rw-r--r-- 2015-07-18 20:47 +0200 15577 Function_Growth.thy
-rw-r--r-- 2015-07-18 20:47 +0200 44411 Fundamental_Theorem_Algebra.thy
-rw-r--r-- 2015-07-18 20:47 +0200 13135 Groups_Big_Fun.thy
-rw-r--r-- 2015-07-18 20:47 +0200 4310 IArray.thy
-rw-r--r-- 2015-07-18 20:47 +0200 7242 Indicator_Function.thy
-rw-r--r-- 2015-07-18 20:47 +0200 16243 Infinite_Set.thy
-rw-r--r-- 2015-07-18 20:47 +0200 13184 Inner_Product.thy
-rw-r--r-- 2015-07-18 20:47 +0200 3785 LaTeXsugar.thy
-rw-r--r-- 2015-07-18 20:47 +0200 19325 Lattice_Algebras.thy
-rw-r--r-- 2015-07-18 20:47 +0200 13707 Lattice_Constructions.thy
-rw-r--r-- 2015-07-18 20:47 +0200 837 Lattice_Syntax.thy
-rw-r--r-- 2015-07-18 20:47 +0200 1148 Library.thy
-rw-r--r-- 2015-07-18 20:47 +0200 12643 Liminf_Limsup.thy
-rw-r--r-- 2015-07-18 20:47 +0200 28515 Linear_Temporal_Logic_on_Streams.thy
-rw-r--r-- 2015-07-18 20:47 +0200 4110 ListVector.thy
-rw-r--r-- 2015-07-18 20:47 +0200 3336 List_lexord.thy
-rw-r--r-- 2015-07-18 20:47 +0200 10127 Lub_Glb.thy
-rw-r--r-- 2015-07-18 20:47 +0200 14418 Mapping.thy
-rw-r--r-- 2015-07-18 20:47 +0200 2293 Monad_Syntax.thy
-rw-r--r-- 2015-07-18 20:47 +0200 12328 More_List.thy
-rw-r--r-- 2015-07-18 20:47 +0200 89968 Multiset.thy
-rw-r--r-- 2015-07-18 20:47 +0200 13802 Multiset_Order.thy
-rw-r--r-- 2015-07-18 20:47 +0200 12362 Nat_Bijection.thy
-rw-r--r-- 2015-07-18 20:47 +0200 17205 Numeral_Type.thy
-rw-r--r-- 2015-07-18 20:47 +0200 14833 Old_Datatype.thy
-rw-r--r-- 2015-07-18 20:47 +0200 1926 Old_Recdef.thy
-rw-r--r-- 2015-07-18 20:47 +0200 14559 Old_SMT.thy
-rw-r--r-- 2015-07-18 20:47 +0200 12600 Option_ord.thy
-rw-r--r-- 2015-07-18 20:47 +0200 2098 OptionalSugar.thy
-rw-r--r-- 2015-07-18 20:47 +0200 16782 Order_Continuity.thy
-rw-r--r-- 2015-07-18 20:47 +0200 1618 Parallel.thy
-rw-r--r-- 2015-07-18 20:47 +0200 8569 Permutation.thy
-rw-r--r-- 2015-07-18 20:47 +0200 35289 Permutations.thy
-rw-r--r-- 2015-07-18 20:47 +0200 1178 Phantom_Type.thy
-rw-r--r-- 2015-07-18 20:47 +0200 11575 Poly_Deriv.thy
-rw-r--r-- 2015-07-18 20:47 +0200 61231 Polynomial.thy
-rw-r--r-- 2015-07-18 20:47 +0200 8060 Predicate_Compile_Alternative_Defs.thy
-rw-r--r-- 2015-07-18 20:47 +0200 289 Predicate_Compile_Quickcheck.thy
-rw-r--r-- 2015-07-18 20:47 +0200 1705 Prefix_Order.thy
-rw-r--r-- 2015-07-18 20:47 +0200 1883 Preorder.thy
-rw-r--r-- 2015-07-18 20:47 +0200 3359 Product_Lexorder.thy
-rw-r--r-- 2015-07-18 20:47 +0200 6488 Product_Order.thy
-rw-r--r-- 2015-07-18 20:47 +0200 22731 Product_Vector.thy
-rw-r--r-- 2015-07-18 20:47 +0200 3381 Product_plus.thy
-rw-r--r-- 2015-07-18 20:47 +0200 6815 Quadratic_Discriminant.thy
-rw-r--r-- 2015-07-18 20:47 +0200 6931 Quotient_List.thy
-rw-r--r-- 2015-07-18 20:47 +0200 2482 Quotient_Option.thy
-rw-r--r-- 2015-07-18 20:47 +0200 3679 Quotient_Product.thy
-rw-r--r-- 2015-07-18 20:47 +0200 3628 Quotient_Set.thy
-rw-r--r-- 2015-07-18 20:47 +0200 2921 Quotient_Sum.thy
-rw-r--r-- 2015-07-18 20:47 +0200 318 Quotient_Syntax.thy
-rw-r--r-- 2015-07-18 20:47 +0200 6885 Quotient_Type.thy
-rw-r--r-- 2015-07-18 20:47 +0200 6620 RBT.thy
-rw-r--r-- 2015-07-18 20:47 +0200 97631 RBT_Impl.thy
-rw-r--r-- 2015-07-18 20:47 +0200 5784 RBT_Mapping.thy
-rw-r--r-- 2015-07-18 20:47 +0200 29392 RBT_Set.thy
-rw-r--r-- 2015-07-18 20:47 +0200 2666 README.html
-rw-r--r-- 2015-07-18 20:47 +0200 17965 Ramsey.thy
-rw-r--r-- 2015-07-18 20:47 +0200 1138 Reflection.thy
-rw-r--r-- 2015-07-18 20:47 +0200 6525 Refute.thy
-rw-r--r-- 2015-07-18 20:47 +0200 1237 Rewrite.thy
-rw-r--r-- 2015-07-18 20:47 +0200 7256 Saturated.thy
-rw-r--r-- 2015-07-18 20:47 +0200 13477 Set_Algebras.thy
-rw-r--r-- 2015-07-18 20:47 +0200 240 Simps_Case_Conv.thy
-rw-r--r-- 2015-07-18 20:47 +0200 5401 State_Monad.thy
-rw-r--r-- 2015-07-18 20:47 +0200 22042 Stream.thy
-rw-r--r-- 2015-07-18 20:47 +0200 25984 Sublist.thy
-rw-r--r-- 2015-07-18 20:47 +0200 2930 Sublist_Order.thy
-rw-r--r-- 2015-07-18 20:47 +0200 535 Sum_of_Squares.thy
-rw-r--r-- 2015-07-18 20:47 +0200 1157 Sum_of_Squares_Remote.thy
-rw-r--r-- 2015-07-18 20:47 +0200 7043 Transitive_Closure_Table.thy
-rw-r--r-- 2015-07-18 20:47 +0200 7276 Tree.thy
-rw-r--r-- 2015-07-18 20:47 +0200 1464 Tree_Multiset.thy
-rw-r--r-- 2015-07-18 20:47 +0200 15330 While_Combinator.thy
-rw-r--r-- 2015-07-18 20:47 +0200 5463 bnf_axiomatization.ML
-rw-r--r-- 2015-07-18 20:47 +0200 7776 bnf_lfp_countable.ML
-rw-r--r-- 2015-07-18 20:47 +0200 8448 cconv.ML
-rw-r--r-- 2015-07-18 20:47 +0200 21222 code_test.ML
-rw-r--r-- 2015-07-18 20:47 +0200 111517 old_recdef.ML
-rw-r--r-- 2015-07-18 20:47 +0200 33106 positivstellensatz.ML
-rw-r--r-- 2015-07-18 20:47 +0200 145257 refute.ML
-rw-r--r-- 2015-07-18 20:47 +0200 17001 rewrite.ML
-rw-r--r-- 2015-07-18 20:47 +0200 8358 simps_case_conv.ML