/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-08-11 15:36 +0200 27959 AList.thy
-rw-r--r-- 2016-08-11 15:36 +0200 4392 AList_Mapping.thy
-rw-r--r-- 2016-08-11 15:36 +0200 387 BNF_Axiomatization.thy
-rw-r--r-- 2016-08-11 15:36 +0200 8365 BNF_Corec.thy
-rw-r--r-- 2016-08-11 15:36 +0200 29551 BigO.thy
-rw-r--r-- 2016-08-11 15:36 +0200 4426 Bit.thy
-rw-r--r-- 2016-08-11 15:36 +0200 11666 Boolean_Algebra.thy
-rw-r--r-- 2016-08-11 15:36 +0200 16852 Bourbaki_Witt_Fixpoint.thy
-rw-r--r-- 2016-08-11 15:36 +0200 793 Cardinal_Notations.thy
-rw-r--r-- 2016-08-11 15:36 +0200 20813 Cardinality.thy
-rw-r--r-- 2016-08-11 15:36 +0200 2284 Char_ord.thy
-rw-r--r-- 2016-08-11 15:36 +0200 3742 Code_Abstract_Nat.thy
-rw-r--r-- 2016-08-11 15:36 +0200 4826 Code_Binary_Nat.thy
-rw-r--r-- 2016-08-11 15:36 +0200 3612 Code_Char.thy
-rw-r--r-- 2016-08-11 15:36 +0200 494 Code_Prolog.thy
-rw-r--r-- 2016-08-11 15:36 +0200 6195 Code_Real_Approx_By_Float.thy
-rw-r--r-- 2016-08-11 15:36 +0200 3134 Code_Target_Int.thy
-rw-r--r-- 2016-08-11 15:36 +0200 4260 Code_Target_Nat.thy
-rw-r--r-- 2016-08-11 15:36 +0200 278 Code_Target_Numeral.thy
-rw-r--r-- 2016-08-11 15:36 +0200 5795 Code_Test.thy
-rw-r--r-- 2016-08-11 15:36 +0200 2117 Combine_PER.thy
-rw-r--r-- 2016-08-11 15:36 +0200 78331 Complete_Partial_Order2.thy
-rw-r--r-- 2016-08-11 15:36 +0200 7426 Continuum_Not_Denumerable.thy
-rw-r--r-- 2016-08-11 15:36 +0200 39442 Convex.thy
-rw-r--r-- 2016-08-11 15:36 +0200 10541 Countable.thy
-rw-r--r-- 2016-08-11 15:36 +0200 12723 Countable_Complete_Lattices.thy
-rw-r--r-- 2016-08-11 15:36 +0200 16306 Countable_Set.thy
-rw-r--r-- 2016-08-11 15:36 +0200 29866 Countable_Set_Type.thy
-rw-r--r-- 2016-08-11 15:36 +0200 6532 DAList.thy
-rw-r--r-- 2016-08-11 15:36 +0200 16723 DAList_Multiset.thy
-rw-r--r-- 2016-08-11 15:36 +0200 1226 Debug.thy
-rw-r--r-- 2016-08-11 15:36 +0200 4017 Diagonal_Subsequence.thy
-rw-r--r-- 2016-08-11 15:36 +0200 7454 Discrete.thy
-rw-r--r-- 2016-08-11 15:36 +0200 14990 Disjoint_Sets.thy
-rw-r--r-- 2016-08-11 15:36 +0200 12684 Dlist.thy
-rw-r--r-- 2016-08-11 15:36 +0200 5193 Extended.thy
-rw-r--r-- 2016-08-11 15:36 +0200 23001 Extended_Nat.thy
-rw-r--r-- 2016-08-11 15:36 +0200 84626 Extended_Nonnegative_Real.thy
-rw-r--r-- 2016-08-11 15:36 +0200 154445 Extended_Real.thy
-rw-r--r-- 2016-08-11 15:36 +0200 48572 FSet.thy
-rw-r--r-- 2016-08-11 15:36 +0200 72457 FinFun.thy
-rw-r--r-- 2016-08-11 15:36 +0200 9879 Finite_Lattice.thy
-rw-r--r-- 2016-08-11 15:36 +0200 93634 Float.thy
-rw-r--r-- 2016-08-11 15:36 +0200 175324 Formal_Power_Series.thy
-rw-r--r-- 2016-08-11 15:36 +0200 16182 Fraction_Field.thy
-rw-r--r-- 2016-08-11 15:36 +0200 3572 Fun_Lexorder.thy
-rw-r--r-- 2016-08-11 15:36 +0200 24109 FuncSet.thy
-rw-r--r-- 2016-08-11 15:36 +0200 6290 Function_Algebras.thy
-rw-r--r-- 2016-08-11 15:36 +0200 1724 Function_Division.thy
-rw-r--r-- 2016-08-11 15:36 +0200 18634 Function_Growth.thy
-rw-r--r-- 2016-08-11 15:36 +0200 44284 Fundamental_Theorem_Algebra.thy
-rw-r--r-- 2016-08-11 15:36 +0200 13017 Groups_Big_Fun.thy
-rw-r--r-- 2016-08-11 15:36 +0200 4242 IArray.thy
-rw-r--r-- 2016-08-11 15:36 +0200 8250 Indicator_Function.thy
-rw-r--r-- 2016-08-11 15:36 +0200 15412 Infinite_Set.thy
-rw-r--r-- 2016-08-11 15:36 +0200 14780 Inner_Product.thy
-rw-r--r-- 2016-08-11 15:36 +0200 4075 LaTeXsugar.thy
-rw-r--r-- 2016-08-11 15:36 +0200 19331 Lattice_Algebras.thy
-rw-r--r-- 2016-08-11 15:36 +0200 13708 Lattice_Constructions.thy
-rw-r--r-- 2016-08-11 15:36 +0200 826 Lattice_Syntax.thy
-rw-r--r-- 2016-08-11 15:36 +0200 1355 Library.thy
-rw-r--r-- 2016-08-11 15:36 +0200 23835 Liminf_Limsup.thy
-rw-r--r-- 2016-08-11 15:36 +0200 28002 Linear_Temporal_Logic_on_Streams.thy
-rw-r--r-- 2016-08-11 15:36 +0200 4122 ListVector.thy
-rw-r--r-- 2016-08-11 15:36 +0200 3252 List_lexord.thy
-rw-r--r-- 2016-08-11 15:36 +0200 10169 Lub_Glb.thy
-rw-r--r-- 2016-08-11 15:36 +0200 26986 Mapping.thy
-rw-r--r-- 2016-08-11 15:36 +0200 2184 Monad_Syntax.thy
-rw-r--r-- 2016-08-11 15:36 +0200 12323 More_List.thy
-rw-r--r-- 2016-08-11 15:36 +0200 122689 Multiset.thy
-rw-r--r-- 2016-08-11 15:36 +0200 11433 Multiset_Order.thy
-rw-r--r-- 2016-08-11 15:36 +0200 12645 Nat_Bijection.thy
-rw-r--r-- 2016-08-11 15:36 +0200 15236 Nonpos_Ints.thy
-rw-r--r-- 2016-08-11 15:36 +0200 17601 Normalized_Fraction.thy
-rw-r--r-- 2016-08-11 15:36 +0200 17040 Numeral_Type.thy
-rw-r--r-- 2016-08-11 15:36 +0200 14727 Old_Datatype.thy
-rw-r--r-- 2016-08-11 15:36 +0200 1926 Old_Recdef.thy
-rw-r--r-- 2016-08-11 15:36 +0200 14688 Old_SMT.thy
-rw-r--r-- 2016-08-11 15:36 +0200 32033 Omega_Words_Fun.thy
-rw-r--r-- 2016-08-11 15:36 +0200 12633 Option_ord.thy
-rw-r--r-- 2016-08-11 15:36 +0200 2222 OptionalSugar.thy
-rw-r--r-- 2016-08-11 15:36 +0200 18359 Order_Continuity.thy
-rw-r--r-- 2016-08-11 15:36 +0200 1618 Parallel.thy
-rw-r--r-- 2016-08-11 15:36 +0200 5334 Periodic_Fun.thy
-rw-r--r-- 2016-08-11 15:36 +0200 26307 Perm.thy
-rw-r--r-- 2016-08-11 15:36 +0200 9365 Permutation.thy
-rw-r--r-- 2016-08-11 15:36 +0200 49777 Permutations.thy
-rw-r--r-- 2016-08-11 15:36 +0200 1178 Phantom_Type.thy
-rw-r--r-- 2016-08-11 15:36 +0200 144154 Polynomial.thy
-rw-r--r-- 2016-08-11 15:36 +0200 12767 Polynomial_FPS.thy
-rw-r--r-- 2016-08-11 15:36 +0200 4801 Polynomial_GCD_euclidean.thy
-rw-r--r-- 2016-08-11 15:36 +0200 8943 Predicate_Compile_Alternative_Defs.thy
-rw-r--r-- 2016-08-11 15:36 +0200 289 Predicate_Compile_Quickcheck.thy
-rw-r--r-- 2016-08-11 15:36 +0200 1907 Prefix_Order.thy
-rw-r--r-- 2016-08-11 15:36 +0200 1699 Preorder.thy
-rw-r--r-- 2016-08-11 15:36 +0200 3359 Product_Lexorder.thy
-rw-r--r-- 2016-08-11 15:36 +0200 9610 Product_Order.thy
-rw-r--r-- 2016-08-11 15:36 +0200 14280 Product_Vector.thy
-rw-r--r-- 2016-08-11 15:36 +0200 3381 Product_plus.thy
-rw-r--r-- 2016-08-11 15:36 +0200 6753 Quadratic_Discriminant.thy
-rw-r--r-- 2016-08-11 15:36 +0200 6859 Quotient_List.thy
-rw-r--r-- 2016-08-11 15:36 +0200 2477 Quotient_Option.thy
-rw-r--r-- 2016-08-11 15:36 +0200 3698 Quotient_Product.thy
-rw-r--r-- 2016-08-11 15:36 +0200 3623 Quotient_Set.thy
-rw-r--r-- 2016-08-11 15:36 +0200 2916 Quotient_Sum.thy
-rw-r--r-- 2016-08-11 15:36 +0200 318 Quotient_Syntax.thy
-rw-r--r-- 2016-08-11 15:36 +0200 6915 Quotient_Type.thy
-rw-r--r-- 2016-08-11 15:36 +0200 8564 RBT.thy
-rw-r--r-- 2016-08-11 15:36 +0200 97738 RBT_Impl.thy
-rw-r--r-- 2016-08-11 15:36 +0200 6554 RBT_Mapping.thy
-rw-r--r-- 2016-08-11 15:36 +0200 29416 RBT_Set.thy
-rw-r--r-- 2016-08-11 15:36 +0200 2666 README.html
-rw-r--r-- 2016-08-11 15:36 +0200 17978 Ramsey.thy
-rw-r--r-- 2016-08-11 15:36 +0200 1131 Reflection.thy
-rw-r--r-- 2016-08-11 15:36 +0200 6529 Refute.thy
-rw-r--r-- 2016-08-11 15:36 +0200 1189 Rewrite.thy
-rw-r--r-- 2016-08-11 15:36 +0200 7273 Saturated.thy
-rw-r--r-- 2016-08-11 15:36 +0200 13819 Set_Algebras.thy
-rw-r--r-- 2016-08-11 15:36 +0200 10248 Set_Permutations.thy
-rw-r--r-- 2016-08-11 15:36 +0200 270 Simps_Case_Conv.thy
-rw-r--r-- 2016-08-11 15:36 +0200 5459 State_Monad.thy
-rw-r--r-- 2016-08-11 15:36 +0200 10931 Stirling.thy
-rw-r--r-- 2016-08-11 15:36 +0200 22437 Stream.thy
-rw-r--r-- 2016-08-11 15:36 +0200 32315 Sublist.thy
-rw-r--r-- 2016-08-11 15:36 +0200 2962 Sublist_Order.thy
-rw-r--r-- 2016-08-11 15:36 +0200 535 Sum_of_Squares.thy
-rw-r--r-- 2016-08-11 15:36 +0200 8225 Transitive_Closure_Table.thy
-rw-r--r-- 2016-08-11 15:36 +0200 8156 Tree.thy
-rw-r--r-- 2016-08-11 15:36 +0200 1187 Tree_Multiset.thy
-rw-r--r-- 2016-08-11 15:36 +0200 18129 While_Combinator.thy
-rw-r--r-- 2016-08-11 15:36 +0200 8448 cconv.ML
-rw-r--r-- 2016-08-11 15:36 +0200 21216 code_test.ML
-rw-r--r-- 2016-08-11 15:36 +0200 110372 old_recdef.ML
-rw-r--r-- 2016-08-11 15:36 +0200 32934 positivstellensatz.ML
-rw-r--r-- 2016-08-11 15:36 +0200 145253 refute.ML
-rw-r--r-- 2016-08-11 15:36 +0200 16992 rewrite.ML
-rw-r--r-- 2016-08-11 15:36 +0200 8380 simps_case_conv.ML