/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-10-27 15:17 +0000 27762 AList.thy
-rw-r--r-- 2015-10-27 15:17 +0000 2365 AList_Mapping.thy
-rw-r--r-- 2015-10-27 15:17 +0000 374 BNF_Axiomatization.thy
-rw-r--r-- 2015-10-27 15:17 +0000 28949 BigO.thy
-rw-r--r-- 2015-10-27 15:17 +0000 4439 Bit.thy
-rw-r--r-- 2015-10-27 15:17 +0000 11479 Boolean_Algebra.thy
-rw-r--r-- 2015-10-27 15:17 +0000 793 Cardinal_Notations.thy
-rw-r--r-- 2015-10-27 15:17 +0000 21293 Cardinality.thy
-rw-r--r-- 2015-10-27 15:17 +0000 3810 Char_ord.thy
-rw-r--r-- 2015-10-27 15:17 +0000 3742 Code_Abstract_Nat.thy
-rw-r--r-- 2015-10-27 15:17 +0000 4826 Code_Binary_Nat.thy
-rw-r--r-- 2015-10-27 15:17 +0000 4467 Code_Char.thy
-rw-r--r-- 2015-10-27 15:17 +0000 494 Code_Prolog.thy
-rw-r--r-- 2015-10-27 15:17 +0000 5910 Code_Real_Approx_By_Float.thy
-rw-r--r-- 2015-10-27 15:17 +0000 2799 Code_Target_Int.thy
-rw-r--r-- 2015-10-27 15:17 +0000 4252 Code_Target_Nat.thy
-rw-r--r-- 2015-10-27 15:17 +0000 278 Code_Target_Numeral.thy
-rw-r--r-- 2015-10-27 15:17 +0000 5759 Code_Test.thy
-rw-r--r-- 2015-10-27 15:17 +0000 5918 ContNotDenum.thy
-rw-r--r-- 2015-10-27 15:17 +0000 32986 Convex.thy
-rw-r--r-- 2015-10-27 15:17 +0000 10513 Countable.thy
-rw-r--r-- 2015-10-27 15:17 +0000 15192 Countable_Set.thy
-rw-r--r-- 2015-10-27 15:17 +0000 29926 Countable_Set_Type.thy
-rw-r--r-- 2015-10-27 15:17 +0000 6528 DAList.thy
-rw-r--r-- 2015-10-27 15:17 +0000 15579 DAList_Multiset.thy
-rw-r--r-- 2015-10-27 15:17 +0000 1218 Debug.thy
-rw-r--r-- 2015-10-27 15:17 +0000 4017 Diagonal_Subsequence.thy
-rw-r--r-- 2015-10-27 15:17 +0000 6040 Discrete.thy
-rw-r--r-- 2015-10-27 15:17 +0000 6560 Disjoint_Sets.thy
-rw-r--r-- 2015-10-27 15:17 +0000 6195 Dlist.thy
-rw-r--r-- 2015-10-27 15:17 +0000 5193 Extended.thy
-rw-r--r-- 2015-10-27 15:17 +0000 21765 Extended_Nat.thy
-rw-r--r-- 2015-10-27 15:17 +0000 134285 Extended_Real.thy
-rw-r--r-- 2015-10-27 15:17 +0000 47714 FSet.thy
-rw-r--r-- 2015-10-27 15:17 +0000 72005 FinFun.thy
-rw-r--r-- 2015-10-27 15:17 +0000 577 FinFun_Syntax.thy
-rw-r--r-- 2015-10-27 15:17 +0000 10013 Finite_Lattice.thy
-rw-r--r-- 2015-10-27 15:17 +0000 89140 Float.thy
-rw-r--r-- 2015-10-27 15:17 +0000 135942 Formal_Power_Series.thy
-rw-r--r-- 2015-10-27 15:17 +0000 16188 Fraction_Field.thy
-rw-r--r-- 2015-10-27 15:17 +0000 3551 Fun_Lexorder.thy
-rw-r--r-- 2015-10-27 15:17 +0000 24166 FuncSet.thy
-rw-r--r-- 2015-10-27 15:17 +0000 5847 Function_Algebras.thy
-rw-r--r-- 2015-10-27 15:17 +0000 1724 Function_Division.thy
-rw-r--r-- 2015-10-27 15:17 +0000 15577 Function_Growth.thy
-rw-r--r-- 2015-10-27 15:17 +0000 44411 Fundamental_Theorem_Algebra.thy
-rw-r--r-- 2015-10-27 15:17 +0000 12875 Groups_Big_Fun.thy
-rw-r--r-- 2015-10-27 15:17 +0000 4256 IArray.thy
-rw-r--r-- 2015-10-27 15:17 +0000 7242 Indicator_Function.thy
-rw-r--r-- 2015-10-27 15:17 +0000 16628 Infinite_Set.thy
-rw-r--r-- 2015-10-27 15:17 +0000 14255 Inner_Product.thy
-rw-r--r-- 2015-10-27 15:17 +0000 3785 LaTeXsugar.thy
-rw-r--r-- 2015-10-27 15:17 +0000 19325 Lattice_Algebras.thy
-rw-r--r-- 2015-10-27 15:17 +0000 13707 Lattice_Constructions.thy
-rw-r--r-- 2015-10-27 15:17 +0000 837 Lattice_Syntax.thy
-rw-r--r-- 2015-10-27 15:17 +0000 1166 Library.thy
-rw-r--r-- 2015-10-27 15:17 +0000 14347 Liminf_Limsup.thy
-rw-r--r-- 2015-10-27 15:17 +0000 27915 Linear_Temporal_Logic_on_Streams.thy
-rw-r--r-- 2015-10-27 15:17 +0000 4110 ListVector.thy
-rw-r--r-- 2015-10-27 15:17 +0000 3252 List_lexord.thy
-rw-r--r-- 2015-10-27 15:17 +0000 10127 Lub_Glb.thy
-rw-r--r-- 2015-10-27 15:17 +0000 14433 Mapping.thy
-rw-r--r-- 2015-10-27 15:17 +0000 2293 Monad_Syntax.thy
-rw-r--r-- 2015-10-27 15:17 +0000 12328 More_List.thy
-rw-r--r-- 2015-10-27 15:17 +0000 91451 Multiset.thy
-rw-r--r-- 2015-10-27 15:17 +0000 13605 Multiset_Order.thy
-rw-r--r-- 2015-10-27 15:17 +0000 12362 Nat_Bijection.thy
-rw-r--r-- 2015-10-27 15:17 +0000 17205 Numeral_Type.thy
-rw-r--r-- 2015-10-27 15:17 +0000 14833 Old_Datatype.thy
-rw-r--r-- 2015-10-27 15:17 +0000 1926 Old_Recdef.thy
-rw-r--r-- 2015-10-27 15:17 +0000 14559 Old_SMT.thy
-rw-r--r-- 2015-10-27 15:17 +0000 31926 Omega_Words_Fun.thy
-rw-r--r-- 2015-10-27 15:17 +0000 12600 Option_ord.thy
-rw-r--r-- 2015-10-27 15:17 +0000 2055 OptionalSugar.thy
-rw-r--r-- 2015-10-27 15:17 +0000 16782 Order_Continuity.thy
-rw-r--r-- 2015-10-27 15:17 +0000 1618 Parallel.thy
-rw-r--r-- 2015-10-27 15:17 +0000 8569 Permutation.thy
-rw-r--r-- 2015-10-27 15:17 +0000 35297 Permutations.thy
-rw-r--r-- 2015-10-27 15:17 +0000 1178 Phantom_Type.thy
-rw-r--r-- 2015-10-27 15:17 +0000 11569 Poly_Deriv.thy
-rw-r--r-- 2015-10-27 15:17 +0000 61244 Polynomial.thy
-rw-r--r-- 2015-10-27 15:17 +0000 8770 Predicate_Compile_Alternative_Defs.thy
-rw-r--r-- 2015-10-27 15:17 +0000 289 Predicate_Compile_Quickcheck.thy
-rw-r--r-- 2015-10-27 15:17 +0000 1697 Prefix_Order.thy
-rw-r--r-- 2015-10-27 15:17 +0000 1709 Preorder.thy
-rw-r--r-- 2015-10-27 15:17 +0000 3359 Product_Lexorder.thy
-rw-r--r-- 2015-10-27 15:17 +0000 6493 Product_Order.thy
-rw-r--r-- 2015-10-27 15:17 +0000 22731 Product_Vector.thy
-rw-r--r-- 2015-10-27 15:17 +0000 3381 Product_plus.thy
-rw-r--r-- 2015-10-27 15:17 +0000 6815 Quadratic_Discriminant.thy
-rw-r--r-- 2015-10-27 15:17 +0000 6931 Quotient_List.thy
-rw-r--r-- 2015-10-27 15:17 +0000 2482 Quotient_Option.thy
-rw-r--r-- 2015-10-27 15:17 +0000 3703 Quotient_Product.thy
-rw-r--r-- 2015-10-27 15:17 +0000 3628 Quotient_Set.thy
-rw-r--r-- 2015-10-27 15:17 +0000 2921 Quotient_Sum.thy
-rw-r--r-- 2015-10-27 15:17 +0000 318 Quotient_Syntax.thy
-rw-r--r-- 2015-10-27 15:17 +0000 6898 Quotient_Type.thy
-rw-r--r-- 2015-10-27 15:17 +0000 6555 RBT.thy
-rw-r--r-- 2015-10-27 15:17 +0000 97793 RBT_Impl.thy
-rw-r--r-- 2015-10-27 15:17 +0000 5778 RBT_Mapping.thy
-rw-r--r-- 2015-10-27 15:17 +0000 29380 RBT_Set.thy
-rw-r--r-- 2015-10-27 15:17 +0000 2666 README.html
-rw-r--r-- 2015-10-27 15:17 +0000 17965 Ramsey.thy
-rw-r--r-- 2015-10-27 15:17 +0000 1131 Reflection.thy
-rw-r--r-- 2015-10-27 15:17 +0000 6525 Refute.thy
-rw-r--r-- 2015-10-27 15:17 +0000 1189 Rewrite.thy
-rw-r--r-- 2015-10-27 15:17 +0000 7269 Saturated.thy
-rw-r--r-- 2015-10-27 15:17 +0000 13471 Set_Algebras.thy
-rw-r--r-- 2015-10-27 15:17 +0000 240 Simps_Case_Conv.thy
-rw-r--r-- 2015-10-27 15:17 +0000 5401 State_Monad.thy
-rw-r--r-- 2015-10-27 15:17 +0000 22050 Stream.thy
-rw-r--r-- 2015-10-27 15:17 +0000 25978 Sublist.thy
-rw-r--r-- 2015-10-27 15:17 +0000 2930 Sublist_Order.thy
-rw-r--r-- 2015-10-27 15:17 +0000 535 Sum_of_Squares.thy
-rw-r--r-- 2015-10-27 15:17 +0000 1157 Sum_of_Squares_Remote.thy
-rw-r--r-- 2015-10-27 15:17 +0000 7043 Transitive_Closure_Table.thy
-rw-r--r-- 2015-10-27 15:17 +0000 5282 Tree.thy
-rw-r--r-- 2015-10-27 15:17 +0000 1187 Tree_Multiset.thy
-rw-r--r-- 2015-10-27 15:17 +0000 15257 While_Combinator.thy
-rw-r--r-- 2015-10-27 15:17 +0000 5505 bnf_axiomatization.ML
-rw-r--r-- 2015-10-27 15:17 +0000 7791 bnf_lfp_countable.ML
-rw-r--r-- 2015-10-27 15:17 +0000 8448 cconv.ML
-rw-r--r-- 2015-10-27 15:17 +0000 21219 code_test.ML
-rw-r--r-- 2015-10-27 15:17 +0000 110379 old_recdef.ML
-rw-r--r-- 2015-10-27 15:17 +0000 33211 positivstellensatz.ML
-rw-r--r-- 2015-10-27 15:17 +0000 145256 refute.ML
-rw-r--r-- 2015-10-27 15:17 +0000 16994 rewrite.ML
-rw-r--r-- 2015-10-27 15:17 +0000 8358 simps_case_conv.ML