/src/HOL/Library/
drwxr-xr-x [up]
drwxr-xr-x Cancellation
drwxr-xr-x Sum_of_Squares
drwxr-xr-x document
-rw-r--r-- 2017-11-11 18:41 +0000 27959 AList.thy
-rw-r--r-- 2017-11-11 18:41 +0000 4392 AList_Mapping.thy
-rw-r--r-- 2017-11-11 18:41 +0000 387 BNF_Axiomatization.thy
-rw-r--r-- 2017-11-11 18:41 +0000 8582 BNF_Corec.thy
-rw-r--r-- 2017-11-11 18:41 +0000 29484 BigO.thy
-rw-r--r-- 2017-11-11 18:41 +0000 4426 Bit.thy
-rw-r--r-- 2017-11-11 18:41 +0000 11537 Boolean_Algebra.thy
-rw-r--r-- 2017-11-11 18:41 +0000 16861 Bourbaki_Witt_Fixpoint.thy
-rw-r--r-- 2017-11-11 18:41 +0000 4034 Cancellation.thy
-rw-r--r-- 2017-11-11 18:41 +0000 793 Cardinal_Notations.thy
-rw-r--r-- 2017-11-11 18:41 +0000 20813 Cardinality.thy
-rw-r--r-- 2017-11-11 18:41 +0000 2284 Char_ord.thy
-rw-r--r-- 2017-11-11 18:41 +0000 3742 Code_Abstract_Nat.thy
-rw-r--r-- 2017-11-11 18:41 +0000 4682 Code_Binary_Nat.thy
-rw-r--r-- 2017-11-11 18:41 +0000 3614 Code_Char.thy
-rw-r--r-- 2017-11-11 18:41 +0000 494 Code_Prolog.thy
-rw-r--r-- 2017-11-11 18:41 +0000 5857 Code_Real_Approx_By_Float.thy
-rw-r--r-- 2017-11-11 18:41 +0000 3485 Code_Target_Int.thy
-rw-r--r-- 2017-11-11 18:41 +0000 4504 Code_Target_Nat.thy
-rw-r--r-- 2017-11-11 18:41 +0000 278 Code_Target_Numeral.thy
-rw-r--r-- 2017-11-11 18:41 +0000 5851 Code_Test.thy
-rw-r--r-- 2017-11-11 18:41 +0000 2097 Combine_PER.thy
-rw-r--r-- 2017-11-11 18:41 +0000 78450 Complete_Partial_Order2.thy
-rw-r--r-- 2017-11-11 18:41 +0000 10539 Countable.thy
-rw-r--r-- 2017-11-11 18:41 +0000 12723 Countable_Complete_Lattices.thy
-rw-r--r-- 2017-11-11 18:41 +0000 16376 Countable_Set.thy
-rw-r--r-- 2017-11-11 18:41 +0000 29834 Countable_Set_Type.thy
-rw-r--r-- 2017-11-11 18:41 +0000 7079 DAList.thy
-rw-r--r-- 2017-11-11 18:41 +0000 16056 DAList_Multiset.thy
-rw-r--r-- 2017-11-11 18:41 +0000 1226 Debug.thy
-rw-r--r-- 2017-11-11 18:41 +0000 3975 Diagonal_Subsequence.thy
-rw-r--r-- 2017-11-11 18:41 +0000 12750 Discrete.thy
-rw-r--r-- 2017-11-11 18:41 +0000 15708 Disjoint_Sets.thy
-rw-r--r-- 2017-11-11 18:41 +0000 12684 Dlist.thy
-rw-r--r-- 2017-11-11 18:41 +0000 5165 Extended.thy
-rw-r--r-- 2017-11-11 18:41 +0000 22998 Extended_Nat.thy
-rw-r--r-- 2017-11-11 18:41 +0000 85520 Extended_Nonnegative_Real.thy
-rw-r--r-- 2017-11-11 18:41 +0000 157080 Extended_Real.thy
-rw-r--r-- 2017-11-11 18:41 +0000 54252 FSet.thy
-rw-r--r-- 2017-11-11 18:41 +0000 9879 Finite_Lattice.thy
-rw-r--r-- 2017-11-11 18:41 +0000 43171 Finite_Map.thy
-rw-r--r-- 2017-11-11 18:41 +0000 85817 Float.thy
-rw-r--r-- 2017-11-11 18:41 +0000 3572 Fun_Lexorder.thy
-rw-r--r-- 2017-11-11 18:41 +0000 23885 FuncSet.thy
-rw-r--r-- 2017-11-11 18:41 +0000 6290 Function_Algebras.thy
-rw-r--r-- 2017-11-11 18:41 +0000 1724 Function_Division.thy
-rw-r--r-- 2017-11-11 18:41 +0000 6083 Going_To_Filter.thy
-rw-r--r-- 2017-11-11 18:41 +0000 12978 Groups_Big_Fun.thy
-rw-r--r-- 2017-11-11 18:41 +0000 4242 IArray.thy
-rw-r--r-- 2017-11-11 18:41 +0000 8298 Indicator_Function.thy
-rw-r--r-- 2017-11-11 18:41 +0000 15751 Infinite_Set.thy
-rw-r--r-- 2017-11-11 18:41 +0000 5819 LaTeXsugar.thy
-rw-r--r-- 2017-11-11 18:41 +0000 18643 Lattice_Algebras.thy
-rw-r--r-- 2017-11-11 18:41 +0000 13708 Lattice_Constructions.thy
-rw-r--r-- 2017-11-11 18:41 +0000 830 Lattice_Syntax.thy
-rw-r--r-- 2017-11-11 18:41 +0000 1316 Library.thy
-rw-r--r-- 2017-11-11 18:41 +0000 26079 Liminf_Limsup.thy
-rw-r--r-- 2017-11-11 18:41 +0000 28723 Linear_Temporal_Logic_on_Streams.thy
-rw-r--r-- 2017-11-11 18:41 +0000 4118 ListVector.thy
-rw-r--r-- 2017-11-11 18:41 +0000 3252 List_lexord.thy
-rw-r--r-- 2017-11-11 18:41 +0000 10773 Log_Nat.thy
-rw-r--r-- 2017-11-11 18:41 +0000 10169 Lub_Glb.thy
-rw-r--r-- 2017-11-11 18:41 +0000 26946 Mapping.thy
-rw-r--r-- 2017-11-11 18:41 +0000 2184 Monad_Syntax.thy
-rw-r--r-- 2017-11-11 18:41 +0000 13469 More_List.thy
-rw-r--r-- 2017-11-11 18:41 +0000 144988 Multiset.thy
-rw-r--r-- 2017-11-11 18:41 +0000 17499 Multiset_Order.thy
-rw-r--r-- 2017-11-11 18:41 +0000 22221 Multiset_Permutations.thy
-rw-r--r-- 2017-11-11 18:41 +0000 12639 Nat_Bijection.thy
-rw-r--r-- 2017-11-11 18:41 +0000 15236 Nonpos_Ints.thy
-rw-r--r-- 2017-11-11 18:41 +0000 16898 Numeral_Type.thy
-rw-r--r-- 2017-11-11 18:41 +0000 14722 Old_Datatype.thy
-rw-r--r-- 2017-11-11 18:41 +0000 1926 Old_Recdef.thy
-rw-r--r-- 2017-11-11 18:41 +0000 32045 Omega_Words_Fun.thy
-rw-r--r-- 2017-11-11 18:41 +0000 5484 Open_State_Syntax.thy
-rw-r--r-- 2017-11-11 18:41 +0000 12626 Option_ord.thy
-rw-r--r-- 2017-11-11 18:41 +0000 2313 OptionalSugar.thy
-rw-r--r-- 2017-11-11 18:41 +0000 18341 Order_Continuity.thy
-rw-r--r-- 2017-11-11 18:41 +0000 1618 Parallel.thy
-rw-r--r-- 2017-11-11 18:41 +0000 7477 Pattern_Aliases.thy
-rw-r--r-- 2017-11-11 18:41 +0000 5334 Periodic_Fun.thy
-rw-r--r-- 2017-11-11 18:41 +0000 26313 Perm.thy
-rw-r--r-- 2017-11-11 18:41 +0000 9371 Permutation.thy
-rw-r--r-- 2017-11-11 18:41 +0000 55764 Permutations.thy
-rw-r--r-- 2017-11-11 18:41 +0000 1178 Phantom_Type.thy
-rw-r--r-- 2017-11-11 18:41 +0000 9062 Predicate_Compile_Alternative_Defs.thy
-rw-r--r-- 2017-11-11 18:41 +0000 352 Predicate_Compile_Quickcheck.thy
-rw-r--r-- 2017-11-11 18:41 +0000 1907 Prefix_Order.thy
-rw-r--r-- 2017-11-11 18:41 +0000 1694 Preorder.thy
-rw-r--r-- 2017-11-11 18:41 +0000 3359 Product_Lexorder.thy
-rw-r--r-- 2017-11-11 18:41 +0000 9610 Product_Order.thy
-rw-r--r-- 2017-11-11 18:41 +0000 3372 Product_Plus.thy
-rw-r--r-- 2017-11-11 18:41 +0000 6753 Quadratic_Discriminant.thy
-rw-r--r-- 2017-11-11 18:41 +0000 6859 Quotient_List.thy
-rw-r--r-- 2017-11-11 18:41 +0000 2477 Quotient_Option.thy
-rw-r--r-- 2017-11-11 18:41 +0000 3698 Quotient_Product.thy
-rw-r--r-- 2017-11-11 18:41 +0000 3623 Quotient_Set.thy
-rw-r--r-- 2017-11-11 18:41 +0000 2916 Quotient_Sum.thy
-rw-r--r-- 2017-11-11 18:41 +0000 318 Quotient_Syntax.thy
-rw-r--r-- 2017-11-11 18:41 +0000 6915 Quotient_Type.thy
-rw-r--r-- 2017-11-11 18:41 +0000 8564 RBT.thy
-rw-r--r-- 2017-11-11 18:41 +0000 97888 RBT_Impl.thy
-rw-r--r-- 2017-11-11 18:41 +0000 6554 RBT_Mapping.thy
-rw-r--r-- 2017-11-11 18:41 +0000 28609 RBT_Set.thy
-rw-r--r-- 2017-11-11 18:41 +0000 2666 README.html
-rw-r--r-- 2017-11-11 18:41 +0000 18153 Ramsey.thy
-rw-r--r-- 2017-11-11 18:41 +0000 1131 Reflection.thy
-rw-r--r-- 2017-11-11 18:41 +0000 6529 Refute.thy
-rw-r--r-- 2017-11-11 18:41 +0000 1189 Rewrite.thy
-rw-r--r-- 2017-11-11 18:41 +0000 7255 Saturated.thy
-rw-r--r-- 2017-11-11 18:41 +0000 13781 Set_Algebras.thy
-rw-r--r-- 2017-11-11 18:41 +0000 276 Simps_Case_Conv.thy
-rw-r--r-- 2017-11-11 18:41 +0000 7849 State_Monad.thy
-rw-r--r-- 2017-11-11 18:41 +0000 10861 Stirling.thy
-rw-r--r-- 2017-11-11 18:41 +0000 22716 Stream.thy
-rw-r--r-- 2017-11-11 18:41 +0000 52225 Sublist.thy
-rw-r--r-- 2017-11-11 18:41 +0000 2955 Subseq_Order.thy
-rw-r--r-- 2017-11-11 18:41 +0000 535 Sum_of_Squares.thy
-rw-r--r-- 2017-11-11 18:41 +0000 8225 Transitive_Closure_Table.thy
-rw-r--r-- 2017-11-11 18:41 +0000 16971 Tree.thy
-rw-r--r-- 2017-11-11 18:41 +0000 1607 Tree_Multiset.thy
-rw-r--r-- 2017-11-11 18:41 +0000 4296 Tree_Real.thy
-rw-r--r-- 2017-11-11 18:41 +0000 1723 Type_Length.thy
-rw-r--r-- 2017-11-11 18:41 +0000 9187 Uprod.thy
-rw-r--r-- 2017-11-11 18:41 +0000 18129 While_Combinator.thy
-rw-r--r-- 2017-11-11 18:41 +0000 8448 cconv.ML
-rw-r--r-- 2017-11-11 18:41 +0000 21286 code_test.ML
-rw-r--r-- 2017-11-11 18:41 +0000 1233 multiset_simprocs.ML
-rw-r--r-- 2017-11-11 18:41 +0000 110421 old_recdef.ML
-rw-r--r-- 2017-11-11 18:41 +0000 32934 positivstellensatz.ML
-rw-r--r-- 2017-11-11 18:41 +0000 145253 refute.ML
-rw-r--r-- 2017-11-11 18:41 +0000 16992 rewrite.ML
-rw-r--r-- 2017-11-11 18:41 +0000 8380 simps_case_conv.ML