/src/HOL/Library/
drwxr-xr-x [up]
drwxr-xr-x Cancellation
drwxr-xr-x Sum_of_Squares
drwxr-xr-x document
-rw-r--r-- 2018-06-02 22:14 +0200 27997 AList.thy
-rw-r--r-- 2018-06-02 22:14 +0200 4392 AList_Mapping.thy
-rw-r--r-- 2018-06-02 22:14 +0200 386 Adhoc_Overloading.thy
-rw-r--r-- 2018-06-02 22:14 +0200 387 BNF_Axiomatization.thy
-rw-r--r-- 2018-06-02 22:14 +0200 8683 BNF_Corec.thy
-rw-r--r-- 2018-06-02 22:14 +0200 29484 BigO.thy
-rw-r--r-- 2018-06-02 22:14 +0200 4426 Bit.thy
-rw-r--r-- 2018-06-02 22:14 +0200 11537 Boolean_Algebra.thy
-rw-r--r-- 2018-06-02 22:14 +0200 16882 Bourbaki_Witt_Fixpoint.thy
-rw-r--r-- 2018-06-02 22:14 +0200 4033 Cancellation.thy
-rw-r--r-- 2018-06-02 22:14 +0200 793 Cardinal_Notations.thy
-rw-r--r-- 2018-06-02 22:14 +0200 20431 Cardinality.thy
-rw-r--r-- 2018-06-02 22:14 +0200 1473 Char_ord.thy
-rw-r--r-- 2018-06-02 22:14 +0200 3742 Code_Abstract_Nat.thy
-rw-r--r-- 2018-06-02 22:14 +0200 4682 Code_Binary_Nat.thy
-rw-r--r-- 2018-06-02 22:14 +0200 9186 Code_Lazy.thy
-rw-r--r-- 2018-06-02 22:14 +0200 494 Code_Prolog.thy
-rw-r--r-- 2018-06-02 22:14 +0200 5855 Code_Real_Approx_By_Float.thy
-rw-r--r-- 2018-06-02 22:14 +0200 4049 Code_Target_Int.thy
-rw-r--r-- 2018-06-02 22:14 +0200 5052 Code_Target_Nat.thy
-rw-r--r-- 2018-06-02 22:14 +0200 278 Code_Target_Numeral.thy
-rw-r--r-- 2018-06-02 22:14 +0200 5781 Code_Test.thy
-rw-r--r-- 2018-06-02 22:14 +0200 2097 Combine_PER.thy
-rw-r--r-- 2018-06-02 22:14 +0200 78220 Complete_Partial_Order2.thy
-rw-r--r-- 2018-06-02 22:14 +0200 1493 Conditional_Parametricity.thy
-rw-r--r-- 2018-06-02 22:14 +0200 10541 Countable.thy
-rw-r--r-- 2018-06-02 22:14 +0200 12723 Countable_Complete_Lattices.thy
-rw-r--r-- 2018-06-02 22:14 +0200 16381 Countable_Set.thy
-rw-r--r-- 2018-06-02 22:14 +0200 29820 Countable_Set_Type.thy
-rw-r--r-- 2018-06-02 22:14 +0200 7085 DAList.thy
-rw-r--r-- 2018-06-02 22:14 +0200 16179 DAList_Multiset.thy
-rw-r--r-- 2018-06-02 22:14 +0200 4068 Datatype_Records.thy
-rw-r--r-- 2018-06-02 22:14 +0200 1226 Debug.thy
-rw-r--r-- 2018-06-02 22:14 +0200 4063 Diagonal_Subsequence.thy
-rw-r--r-- 2018-06-02 22:14 +0200 12752 Discrete.thy
-rw-r--r-- 2018-06-02 22:14 +0200 15704 Disjoint_Sets.thy
-rw-r--r-- 2018-06-02 22:14 +0200 12681 Dlist.thy
-rw-r--r-- 2018-06-02 22:14 +0200 5170 Extended.thy
-rw-r--r-- 2018-06-02 22:14 +0200 23144 Extended_Nat.thy
-rw-r--r-- 2018-06-02 22:14 +0200 86396 Extended_Nonnegative_Real.thy
-rw-r--r-- 2018-06-02 22:14 +0200 166278 Extended_Real.thy
-rw-r--r-- 2018-06-02 22:14 +0200 54246 FSet.thy
-rw-r--r-- 2018-06-02 22:14 +0200 10453 Finite_Lattice.thy
-rw-r--r-- 2018-06-02 22:14 +0200 43220 Finite_Map.thy
-rw-r--r-- 2018-06-02 22:14 +0200 86161 Float.thy
-rw-r--r-- 2018-06-02 22:14 +0200 3578 Fun_Lexorder.thy
-rw-r--r-- 2018-06-02 22:14 +0200 23885 FuncSet.thy
-rw-r--r-- 2018-06-02 22:14 +0200 6290 Function_Algebras.thy
-rw-r--r-- 2018-06-02 22:14 +0200 1724 Function_Division.thy
-rw-r--r-- 2018-06-02 22:14 +0200 6121 Going_To_Filter.thy
-rw-r--r-- 2018-06-02 22:14 +0200 12978 Groups_Big_Fun.thy
-rw-r--r-- 2018-06-02 22:14 +0200 4261 IArray.thy
-rw-r--r-- 2018-06-02 22:14 +0200 8461 Indicator_Function.thy
-rw-r--r-- 2018-06-02 22:14 +0200 15771 Infinite_Set.thy
-rw-r--r-- 2018-06-02 22:14 +0200 5661 LaTeXsugar.thy
-rw-r--r-- 2018-06-02 22:14 +0200 104935 Landau_Symbols.thy
-rw-r--r-- 2018-06-02 22:14 +0200 18643 Lattice_Algebras.thy
-rw-r--r-- 2018-06-02 22:14 +0200 13708 Lattice_Constructions.thy
-rw-r--r-- 2018-06-02 22:14 +0200 830 Lattice_Syntax.thy
-rw-r--r-- 2018-06-02 22:14 +0200 1393 Library.thy
-rw-r--r-- 2018-06-02 22:14 +0200 26079 Liminf_Limsup.thy
-rw-r--r-- 2018-06-02 22:14 +0200 28785 Linear_Temporal_Logic_on_Streams.thy
-rw-r--r-- 2018-06-02 22:14 +0200 4111 ListVector.thy
-rw-r--r-- 2018-06-02 22:14 +0200 3256 List_Lexorder.thy
-rw-r--r-- 2018-06-02 22:14 +0200 10858 Log_Nat.thy
-rw-r--r-- 2018-06-02 22:14 +0200 10286 Lub_Glb.thy
-rw-r--r-- 2018-06-02 22:14 +0200 26946 Mapping.thy
-rw-r--r-- 2018-06-02 22:14 +0200 2221 Monad_Syntax.thy
-rw-r--r-- 2018-06-02 22:14 +0200 13618 More_List.thy
-rw-r--r-- 2018-06-02 22:14 +0200 145140 Multiset.thy
-rw-r--r-- 2018-06-02 22:14 +0200 17499 Multiset_Order.thy
-rw-r--r-- 2018-06-02 22:14 +0200 22217 Multiset_Permutations.thy
-rw-r--r-- 2018-06-02 22:14 +0200 12638 Nat_Bijection.thy
-rw-r--r-- 2018-06-02 22:14 +0200 15192 Nonpos_Ints.thy
-rw-r--r-- 2018-06-02 22:14 +0200 16893 Numeral_Type.thy
-rw-r--r-- 2018-06-02 22:14 +0200 15316 Old_Datatype.thy
-rw-r--r-- 2018-06-02 22:14 +0200 2372 Old_Recdef.thy
-rw-r--r-- 2018-06-02 22:14 +0200 32175 Omega_Words_Fun.thy
-rw-r--r-- 2018-06-02 22:14 +0200 5483 Open_State_Syntax.thy
-rw-r--r-- 2018-06-02 22:14 +0200 19401 Option_ord.thy
-rw-r--r-- 2018-06-02 22:14 +0200 2313 OptionalSugar.thy
-rw-r--r-- 2018-06-02 22:14 +0200 18341 Order_Continuity.thy
-rw-r--r-- 2018-06-02 22:14 +0200 1618 Parallel.thy
-rw-r--r-- 2018-06-02 22:14 +0200 7482 Pattern_Aliases.thy
-rw-r--r-- 2018-06-02 22:14 +0200 5334 Periodic_Fun.thy
-rw-r--r-- 2018-06-02 22:14 +0200 26311 Perm.thy
-rw-r--r-- 2018-06-02 22:14 +0200 9371 Permutation.thy
-rw-r--r-- 2018-06-02 22:14 +0200 55678 Permutations.thy
-rw-r--r-- 2018-06-02 22:14 +0200 1178 Phantom_Type.thy
-rw-r--r-- 2018-06-02 22:14 +0200 9139 Predicate_Compile_Alternative_Defs.thy
-rw-r--r-- 2018-06-02 22:14 +0200 352 Predicate_Compile_Quickcheck.thy
-rw-r--r-- 2018-06-02 22:14 +0200 1907 Prefix_Order.thy
-rw-r--r-- 2018-06-02 22:14 +0200 1695 Preorder.thy
-rw-r--r-- 2018-06-02 22:14 +0200 3359 Product_Lexorder.thy
-rw-r--r-- 2018-06-02 22:14 +0200 9551 Product_Order.thy
-rw-r--r-- 2018-06-02 22:14 +0200 3372 Product_Plus.thy
-rw-r--r-- 2018-06-02 22:14 +0200 6753 Quadratic_Discriminant.thy
-rw-r--r-- 2018-06-02 22:14 +0200 6834 Quotient_List.thy
-rw-r--r-- 2018-06-02 22:14 +0200 2477 Quotient_Option.thy
-rw-r--r-- 2018-06-02 22:14 +0200 3680 Quotient_Product.thy
-rw-r--r-- 2018-06-02 22:14 +0200 3592 Quotient_Set.thy
-rw-r--r-- 2018-06-02 22:14 +0200 2907 Quotient_Sum.thy
-rw-r--r-- 2018-06-02 22:14 +0200 318 Quotient_Syntax.thy
-rw-r--r-- 2018-06-02 22:14 +0200 6915 Quotient_Type.thy
-rw-r--r-- 2018-06-02 22:14 +0200 8564 RBT.thy
-rw-r--r-- 2018-06-02 22:14 +0200 97666 RBT_Impl.thy
-rw-r--r-- 2018-06-02 22:14 +0200 6554 RBT_Mapping.thy
-rw-r--r-- 2018-06-02 22:14 +0200 28753 RBT_Set.thy
-rw-r--r-- 2018-06-02 22:14 +0200 2666 README.html
-rw-r--r-- 2018-06-02 22:14 +0200 18165 Ramsey.thy
-rw-r--r-- 2018-06-02 22:14 +0200 349 Realizers.thy
-rw-r--r-- 2018-06-02 22:14 +0200 1131 Reflection.thy
-rw-r--r-- 2018-06-02 22:14 +0200 6529 Refute.thy
-rw-r--r-- 2018-06-02 22:14 +0200 1189 Rewrite.thy
-rw-r--r-- 2018-06-02 22:14 +0200 7255 Saturated.thy
-rw-r--r-- 2018-06-02 22:14 +0200 13781 Set_Algebras.thy
-rw-r--r-- 2018-06-02 22:14 +0200 263 Simps_Case_Conv.thy
-rw-r--r-- 2018-06-02 22:14 +0200 7844 State_Monad.thy
-rw-r--r-- 2018-06-02 22:14 +0200 10861 Stirling.thy
-rw-r--r-- 2018-06-02 22:14 +0200 22827 Stream.thy
-rw-r--r-- 2018-06-02 22:14 +0200 52737 Sublist.thy
-rw-r--r-- 2018-06-02 22:14 +0200 2952 Subseq_Order.thy
-rw-r--r-- 2018-06-02 22:14 +0200 535 Sum_of_Squares.thy
-rw-r--r-- 2018-06-02 22:14 +0200 8225 Transitive_Closure_Table.thy
-rw-r--r-- 2018-06-02 22:14 +0200 16931 Tree.thy
-rw-r--r-- 2018-06-02 22:14 +0200 1607 Tree_Multiset.thy
-rw-r--r-- 2018-06-02 22:14 +0200 4297 Tree_Real.thy
-rw-r--r-- 2018-06-02 22:14 +0200 1723 Type_Length.thy
-rw-r--r-- 2018-06-02 22:14 +0200 9181 Uprod.thy
-rw-r--r-- 2018-06-02 22:14 +0200 18271 While_Combinator.thy
-rw-r--r-- 2018-06-02 22:14 +0200 8315 adhoc_overloading.ML
-rw-r--r-- 2018-06-02 22:14 +0200 19907 case_converter.ML
-rw-r--r-- 2018-06-02 22:14 +0200 8448 cconv.ML
-rw-r--r-- 2018-06-02 22:14 +0200 24593 code_lazy.ML
-rw-r--r-- 2018-06-02 22:14 +0200 21304 code_test.ML
-rw-r--r-- 2018-06-02 22:14 +0200 19966 conditional_parametricity.ML
-rw-r--r-- 2018-06-02 22:14 +0200 6662 datatype_records.ML
-rw-r--r-- 2018-06-02 22:14 +0200 1233 multiset_simprocs.ML
-rw-r--r-- 2018-06-02 22:14 +0200 110400 old_recdef.ML
-rw-r--r-- 2018-06-02 22:14 +0200 35402 positivstellensatz.ML
-rw-r--r-- 2018-06-02 22:14 +0200 145229 refute.ML
-rw-r--r-- 2018-06-02 22:14 +0200 16992 rewrite.ML
-rw-r--r-- 2018-06-02 22:14 +0200 8380 simps_case_conv.ML