/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-- 2016-05-23 15:33 +0100 27846 AList.thy
-rw-r--r-- 2016-05-23 15:33 +0100 2365 AList_Mapping.thy
-rw-r--r-- 2016-05-23 15:33 +0100 387 BNF_Axiomatization.thy
-rw-r--r-- 2016-05-23 15:33 +0100 8365 BNF_Corec.thy
-rw-r--r-- 2016-05-23 15:33 +0100 29557 BigO.thy
-rw-r--r-- 2016-05-23 15:33 +0100 4439 Bit.thy
-rw-r--r-- 2016-05-23 15:33 +0100 11476 Boolean_Algebra.thy
-rw-r--r-- 2016-05-23 15:33 +0100 10950 Bourbaki_Witt_Fixpoint.thy
-rw-r--r-- 2016-05-23 15:33 +0100 793 Cardinal_Notations.thy
-rw-r--r-- 2016-05-23 15:33 +0100 20813 Cardinality.thy
-rw-r--r-- 2016-05-23 15:33 +0100 2260 Char_ord.thy
-rw-r--r-- 2016-05-23 15:33 +0100 3742 Code_Abstract_Nat.thy
-rw-r--r-- 2016-05-23 15:33 +0100 4826 Code_Binary_Nat.thy
-rw-r--r-- 2016-05-23 15:33 +0100 3612 Code_Char.thy
-rw-r--r-- 2016-05-23 15:33 +0100 494 Code_Prolog.thy
-rw-r--r-- 2016-05-23 15:33 +0100 5910 Code_Real_Approx_By_Float.thy
-rw-r--r-- 2016-05-23 15:33 +0100 3052 Code_Target_Int.thy
-rw-r--r-- 2016-05-23 15:33 +0100 4260 Code_Target_Nat.thy
-rw-r--r-- 2016-05-23 15:33 +0100 278 Code_Target_Numeral.thy
-rw-r--r-- 2016-05-23 15:33 +0100 5795 Code_Test.thy
-rw-r--r-- 2016-05-23 15:33 +0100 76299 Complete_Partial_Order2.thy
-rw-r--r-- 2016-05-23 15:33 +0100 7263 ContNotDenum.thy
-rw-r--r-- 2016-05-23 15:33 +0100 39336 Convex.thy
-rw-r--r-- 2016-05-23 15:33 +0100 10541 Countable.thy
-rw-r--r-- 2016-05-23 15:33 +0100 12723 Countable_Complete_Lattices.thy
-rw-r--r-- 2016-05-23 15:33 +0100 15666 Countable_Set.thy
-rw-r--r-- 2016-05-23 15:33 +0100 29881 Countable_Set_Type.thy
-rw-r--r-- 2016-05-23 15:33 +0100 6532 DAList.thy
-rw-r--r-- 2016-05-23 15:33 +0100 15601 DAList_Multiset.thy
-rw-r--r-- 2016-05-23 15:33 +0100 1226 Debug.thy
-rw-r--r-- 2016-05-23 15:33 +0100 4017 Diagonal_Subsequence.thy
-rw-r--r-- 2016-05-23 15:33 +0100 7473 Discrete.thy
-rw-r--r-- 2016-05-23 15:33 +0100 14975 Disjoint_Sets.thy
-rw-r--r-- 2016-05-23 15:33 +0100 12373 Dlist.thy
-rw-r--r-- 2016-05-23 15:33 +0100 5193 Extended.thy
-rw-r--r-- 2016-05-23 15:33 +0100 23001 Extended_Nat.thy
-rw-r--r-- 2016-05-23 15:33 +0100 73569 Extended_Nonnegative_Real.thy
-rw-r--r-- 2016-05-23 15:33 +0100 149682 Extended_Real.thy
-rw-r--r-- 2016-05-23 15:33 +0100 47764 FSet.thy
-rw-r--r-- 2016-05-23 15:33 +0100 72038 FinFun.thy
-rw-r--r-- 2016-05-23 15:33 +0100 574 FinFun_Syntax.thy
-rw-r--r-- 2016-05-23 15:33 +0100 9879 Finite_Lattice.thy
-rw-r--r-- 2016-05-23 15:33 +0100 91932 Float.thy
-rw-r--r-- 2016-05-23 15:33 +0100 162192 Formal_Power_Series.thy
-rw-r--r-- 2016-05-23 15:33 +0100 16182 Fraction_Field.thy
-rw-r--r-- 2016-05-23 15:33 +0100 3572 Fun_Lexorder.thy
-rw-r--r-- 2016-05-23 15:33 +0100 24109 FuncSet.thy
-rw-r--r-- 2016-05-23 15:33 +0100 6290 Function_Algebras.thy
-rw-r--r-- 2016-05-23 15:33 +0100 1724 Function_Division.thy
-rw-r--r-- 2016-05-23 15:33 +0100 18643 Function_Growth.thy
-rw-r--r-- 2016-05-23 15:33 +0100 44266 Fundamental_Theorem_Algebra.thy
-rw-r--r-- 2016-05-23 15:33 +0100 12450 Groups_Big_Fun.thy
-rw-r--r-- 2016-05-23 15:33 +0100 4256 IArray.thy
-rw-r--r-- 2016-05-23 15:33 +0100 8079 Indicator_Function.thy
-rw-r--r-- 2016-05-23 15:33 +0100 14134 Infinite_Set.thy
-rw-r--r-- 2016-05-23 15:33 +0100 14776 Inner_Product.thy
-rw-r--r-- 2016-05-23 15:33 +0100 3577 LaTeXsugar.thy
-rw-r--r-- 2016-05-23 15:33 +0100 19331 Lattice_Algebras.thy
-rw-r--r-- 2016-05-23 15:33 +0100 13708 Lattice_Constructions.thy
-rw-r--r-- 2016-05-23 15:33 +0100 826 Lattice_Syntax.thy
-rw-r--r-- 2016-05-23 15:33 +0100 1285 Library.thy
-rw-r--r-- 2016-05-23 15:33 +0100 23835 Liminf_Limsup.thy
-rw-r--r-- 2016-05-23 15:33 +0100 28020 Linear_Temporal_Logic_on_Streams.thy
-rw-r--r-- 2016-05-23 15:33 +0100 4122 ListVector.thy
-rw-r--r-- 2016-05-23 15:33 +0100 3252 List_lexord.thy
-rw-r--r-- 2016-05-23 15:33 +0100 10169 Lub_Glb.thy
-rw-r--r-- 2016-05-23 15:33 +0100 14449 Mapping.thy
-rw-r--r-- 2016-05-23 15:33 +0100 2184 Monad_Syntax.thy
-rw-r--r-- 2016-05-23 15:33 +0100 12333 More_List.thy
-rw-r--r-- 2016-05-23 15:33 +0100 112000 Multiset.thy
-rw-r--r-- 2016-05-23 15:33 +0100 14144 Multiset_Order.thy
-rw-r--r-- 2016-05-23 15:33 +0100 12343 Nat_Bijection.thy
-rw-r--r-- 2016-05-23 15:33 +0100 15236 Nonpos_Ints.thy
-rw-r--r-- 2016-05-23 15:33 +0100 17040 Numeral_Type.thy
-rw-r--r-- 2016-05-23 15:33 +0100 14727 Old_Datatype.thy
-rw-r--r-- 2016-05-23 15:33 +0100 1926 Old_Recdef.thy
-rw-r--r-- 2016-05-23 15:33 +0100 14688 Old_SMT.thy
-rw-r--r-- 2016-05-23 15:33 +0100 32035 Omega_Words_Fun.thy
-rw-r--r-- 2016-05-23 15:33 +0100 12633 Option_ord.thy
-rw-r--r-- 2016-05-23 15:33 +0100 2222 OptionalSugar.thy
-rw-r--r-- 2016-05-23 15:33 +0100 18375 Order_Continuity.thy
-rw-r--r-- 2016-05-23 15:33 +0100 1618 Parallel.thy
-rw-r--r-- 2016-05-23 15:33 +0100 5334 Periodic_Fun.thy
-rw-r--r-- 2016-05-23 15:33 +0100 9357 Permutation.thy
-rw-r--r-- 2016-05-23 15:33 +0100 49718 Permutations.thy
-rw-r--r-- 2016-05-23 15:33 +0100 1178 Phantom_Type.thy
-rw-r--r-- 2016-05-23 15:33 +0100 131587 Polynomial.thy
-rw-r--r-- 2016-05-23 15:33 +0100 4801 Polynomial_GCD_euclidean.thy
-rw-r--r-- 2016-05-23 15:33 +0100 8943 Predicate_Compile_Alternative_Defs.thy
-rw-r--r-- 2016-05-23 15:33 +0100 289 Predicate_Compile_Quickcheck.thy
-rw-r--r-- 2016-05-23 15:33 +0100 1697 Prefix_Order.thy
-rw-r--r-- 2016-05-23 15:33 +0100 1709 Preorder.thy
-rw-r--r-- 2016-05-23 15:33 +0100 3359 Product_Lexorder.thy
-rw-r--r-- 2016-05-23 15:33 +0100 6381 Product_Order.thy
-rw-r--r-- 2016-05-23 15:33 +0100 14280 Product_Vector.thy
-rw-r--r-- 2016-05-23 15:33 +0100 3381 Product_plus.thy
-rw-r--r-- 2016-05-23 15:33 +0100 6829 Quadratic_Discriminant.thy
-rw-r--r-- 2016-05-23 15:33 +0100 6926 Quotient_List.thy
-rw-r--r-- 2016-05-23 15:33 +0100 2477 Quotient_Option.thy
-rw-r--r-- 2016-05-23 15:33 +0100 3698 Quotient_Product.thy
-rw-r--r-- 2016-05-23 15:33 +0100 3623 Quotient_Set.thy
-rw-r--r-- 2016-05-23 15:33 +0100 2916 Quotient_Sum.thy
-rw-r--r-- 2016-05-23 15:33 +0100 318 Quotient_Syntax.thy
-rw-r--r-- 2016-05-23 15:33 +0100 6915 Quotient_Type.thy
-rw-r--r-- 2016-05-23 15:33 +0100 6555 RBT.thy
-rw-r--r-- 2016-05-23 15:33 +0100 97771 RBT_Impl.thy
-rw-r--r-- 2016-05-23 15:33 +0100 5849 RBT_Mapping.thy
-rw-r--r-- 2016-05-23 15:33 +0100 29380 RBT_Set.thy
-rw-r--r-- 2016-05-23 15:33 +0100 2666 README.html
-rw-r--r-- 2016-05-23 15:33 +0100 17978 Ramsey.thy
-rw-r--r-- 2016-05-23 15:33 +0100 1131 Reflection.thy
-rw-r--r-- 2016-05-23 15:33 +0100 6525 Refute.thy
-rw-r--r-- 2016-05-23 15:33 +0100 1189 Rewrite.thy
-rw-r--r-- 2016-05-23 15:33 +0100 7273 Saturated.thy
-rw-r--r-- 2016-05-23 15:33 +0100 13478 Set_Algebras.thy
-rw-r--r-- 2016-05-23 15:33 +0100 240 Simps_Case_Conv.thy
-rw-r--r-- 2016-05-23 15:33 +0100 5448 State_Monad.thy
-rw-r--r-- 2016-05-23 15:33 +0100 10616 Stirling.thy
-rw-r--r-- 2016-05-23 15:33 +0100 22102 Stream.thy
-rw-r--r-- 2016-05-23 15:33 +0100 25978 Sublist.thy
-rw-r--r-- 2016-05-23 15:33 +0100 2958 Sublist_Order.thy
-rw-r--r-- 2016-05-23 15:33 +0100 535 Sum_of_Squares.thy
-rw-r--r-- 2016-05-23 15:33 +0100 8225 Transitive_Closure_Table.thy
-rw-r--r-- 2016-05-23 15:33 +0100 6682 Tree.thy
-rw-r--r-- 2016-05-23 15:33 +0100 1187 Tree_Multiset.thy
-rw-r--r-- 2016-05-23 15:33 +0100 15281 While_Combinator.thy
-rw-r--r-- 2016-05-23 15:33 +0100 8448 cconv.ML
-rw-r--r-- 2016-05-23 15:33 +0100 21209 code_test.ML
-rw-r--r-- 2016-05-23 15:33 +0100 110358 old_recdef.ML
-rw-r--r-- 2016-05-23 15:33 +0100 33183 positivstellensatz.ML
-rw-r--r-- 2016-05-23 15:33 +0100 145253 refute.ML
-rw-r--r-- 2016-05-23 15:33 +0100 16993 rewrite.ML
-rw-r--r-- 2016-05-23 15:33 +0100 8353 simps_case_conv.ML