/src/HOL/Library/
drwxr-xr-x [up]
drwxr-xr-x Cancellation
drwxr-xr-x Sum_of_Squares
drwxr-xr-x document
-rw-r--r-- 2019-01-01 17:04 +0100 27959 AList.thy
-rw-r--r-- 2019-01-01 17:04 +0100 4392 AList_Mapping.thy
-rw-r--r-- 2019-01-01 17:04 +0100 386 Adhoc_Overloading.thy
-rw-r--r-- 2019-01-01 17:04 +0100 387 BNF_Axiomatization.thy
-rw-r--r-- 2019-01-01 17:04 +0100 8683 BNF_Corec.thy
-rw-r--r-- 2019-01-01 17:04 +0100 29440 BigO.thy
-rw-r--r-- 2019-01-01 17:04 +0100 4426 Bit.thy
-rw-r--r-- 2019-01-01 17:04 +0100 11537 Boolean_Algebra.thy
-rw-r--r-- 2019-01-01 17:04 +0100 16882 Bourbaki_Witt_Fixpoint.thy
-rw-r--r-- 2019-01-01 17:04 +0100 4033 Cancellation.thy
-rw-r--r-- 2019-01-01 17:04 +0100 793 Cardinal_Notations.thy
-rw-r--r-- 2019-01-01 17:04 +0100 20366 Cardinality.thy
-rw-r--r-- 2019-01-01 17:04 +0100 671 Case_Converter.thy
-rw-r--r-- 2019-01-01 17:04 +0100 1473 Char_ord.thy
-rw-r--r-- 2019-01-01 17:04 +0100 3741 Code_Abstract_Nat.thy
-rw-r--r-- 2019-01-01 17:04 +0100 4682 Code_Binary_Nat.thy
-rw-r--r-- 2019-01-01 17:04 +0100 8856 Code_Lazy.thy
-rw-r--r-- 2019-01-01 17:04 +0100 494 Code_Prolog.thy
-rw-r--r-- 2019-01-01 17:04 +0100 5853 Code_Real_Approx_By_Float.thy
-rw-r--r-- 2019-01-01 17:04 +0100 4049 Code_Target_Int.thy
-rw-r--r-- 2019-01-01 17:04 +0100 5052 Code_Target_Nat.thy
-rw-r--r-- 2019-01-01 17:04 +0100 278 Code_Target_Numeral.thy
-rw-r--r-- 2019-01-01 17:04 +0100 5787 Code_Test.thy
-rw-r--r-- 2019-01-01 17:04 +0100 2097 Combine_PER.thy
-rw-r--r-- 2019-01-01 17:04 +0100 9338 Comparator.thy
-rw-r--r-- 2019-01-01 17:04 +0100 78205 Complete_Partial_Order2.thy
-rw-r--r-- 2019-01-01 17:04 +0100 1493 Conditional_Parametricity.thy
-rw-r--r-- 2019-01-01 17:04 +0100 10626 Countable.thy
-rw-r--r-- 2019-01-01 17:04 +0100 13024 Countable_Complete_Lattices.thy
-rw-r--r-- 2019-01-01 17:04 +0100 16567 Countable_Set.thy
-rw-r--r-- 2019-01-01 17:04 +0100 29581 Countable_Set_Type.thy
-rw-r--r-- 2019-01-01 17:04 +0100 7085 DAList.thy
-rw-r--r-- 2019-01-01 17:04 +0100 16173 DAList_Multiset.thy
-rw-r--r-- 2019-01-01 17:04 +0100 4068 Datatype_Records.thy
-rw-r--r-- 2019-01-01 17:04 +0100 1226 Debug.thy
-rw-r--r-- 2019-01-01 17:04 +0100 4063 Diagonal_Subsequence.thy
-rw-r--r-- 2019-01-01 17:04 +0100 12748 Discrete.thy
-rw-r--r-- 2019-01-01 17:04 +0100 15728 Disjoint_Sets.thy
-rw-r--r-- 2019-01-01 17:04 +0100 12681 Dlist.thy
-rw-r--r-- 2019-01-01 17:04 +0100 5170 Extended.thy
-rw-r--r-- 2019-01-01 17:04 +0100 23128 Extended_Nat.thy
-rw-r--r-- 2019-01-01 17:04 +0100 85555 Extended_Nonnegative_Real.thy
-rw-r--r-- 2019-01-01 17:04 +0100 164733 Extended_Real.thy
-rw-r--r-- 2019-01-01 17:04 +0100 54841 FSet.thy
-rw-r--r-- 2019-01-01 17:04 +0100 10461 Finite_Lattice.thy
-rw-r--r-- 2019-01-01 17:04 +0100 51681 Finite_Map.thy
-rw-r--r-- 2019-01-01 17:04 +0100 85771 Float.thy
-rw-r--r-- 2019-01-01 17:04 +0100 3578 Fun_Lexorder.thy
-rw-r--r-- 2019-01-01 17:04 +0100 26509 FuncSet.thy
-rw-r--r-- 2019-01-01 17:04 +0100 6290 Function_Algebras.thy
-rw-r--r-- 2019-01-01 17:04 +0100 1724 Function_Division.thy
-rw-r--r-- 2019-01-01 17:04 +0100 6115 Going_To_Filter.thy
-rw-r--r-- 2019-01-01 17:04 +0100 12839 Groups_Big_Fun.thy
-rw-r--r-- 2019-01-01 17:04 +0100 7789 IArray.thy
-rw-r--r-- 2019-01-01 17:04 +0100 8467 Indicator_Function.thy
-rw-r--r-- 2019-01-01 17:04 +0100 15994 Infinite_Set.thy
-rw-r--r-- 2019-01-01 17:04 +0100 5662 LaTeXsugar.thy
-rw-r--r-- 2019-01-01 17:04 +0100 105077 Landau_Symbols.thy
-rw-r--r-- 2019-01-01 17:04 +0100 18608 Lattice_Algebras.thy
-rw-r--r-- 2019-01-01 17:04 +0100 13708 Lattice_Constructions.thy
-rw-r--r-- 2019-01-01 17:04 +0100 815 Lattice_Syntax.thy
-rw-r--r-- 2019-01-01 17:04 +0100 1427 Library.thy
-rw-r--r-- 2019-01-01 17:04 +0100 26445 Liminf_Limsup.thy
-rw-r--r-- 2019-01-01 17:04 +0100 28762 Linear_Temporal_Logic_on_Streams.thy
-rw-r--r-- 2019-01-01 17:04 +0100 4109 ListVector.thy
-rw-r--r-- 2019-01-01 17:04 +0100 3256 List_Lexorder.thy
-rw-r--r-- 2019-01-01 17:04 +0100 10832 Log_Nat.thy
-rw-r--r-- 2019-01-01 17:04 +0100 10286 Lub_Glb.thy
-rw-r--r-- 2019-01-01 17:04 +0100 26841 Mapping.thy
-rw-r--r-- 2019-01-01 17:04 +0100 2221 Monad_Syntax.thy
-rw-r--r-- 2019-01-01 17:04 +0100 13618 More_List.thy
-rw-r--r-- 2019-01-01 17:04 +0100 144898 Multiset.thy
-rw-r--r-- 2019-01-01 17:04 +0100 17499 Multiset_Order.thy
-rw-r--r-- 2019-01-01 17:04 +0100 22207 Multiset_Permutations.thy
-rw-r--r-- 2019-01-01 17:04 +0100 12638 Nat_Bijection.thy
-rw-r--r-- 2019-01-01 17:04 +0100 15422 Nonpos_Ints.thy
-rw-r--r-- 2019-01-01 17:04 +0100 16891 Numeral_Type.thy
-rw-r--r-- 2019-01-01 17:04 +0100 15316 Old_Datatype.thy
-rw-r--r-- 2019-01-01 17:04 +0100 2372 Old_Recdef.thy
-rw-r--r-- 2019-01-01 17:04 +0100 32155 Omega_Words_Fun.thy
-rw-r--r-- 2019-01-01 17:04 +0100 5483 Open_State_Syntax.thy
-rw-r--r-- 2019-01-01 17:04 +0100 19438 Option_ord.thy
-rw-r--r-- 2019-01-01 17:04 +0100 2313 OptionalSugar.thy
-rw-r--r-- 2019-01-01 17:04 +0100 18340 Order_Continuity.thy
-rw-r--r-- 2019-01-01 17:04 +0100 1618 Parallel.thy
-rw-r--r-- 2019-01-01 17:04 +0100 7482 Pattern_Aliases.thy
-rw-r--r-- 2019-01-01 17:04 +0100 5324 Periodic_Fun.thy
-rw-r--r-- 2019-01-01 17:04 +0100 26289 Perm.thy
-rw-r--r-- 2019-01-01 17:04 +0100 9371 Permutation.thy
-rw-r--r-- 2019-01-01 17:04 +0100 55678 Permutations.thy
-rw-r--r-- 2019-01-01 17:04 +0100 1178 Phantom_Type.thy
-rw-r--r-- 2019-01-01 17:04 +0100 9139 Predicate_Compile_Alternative_Defs.thy
-rw-r--r-- 2019-01-01 17:04 +0100 352 Predicate_Compile_Quickcheck.thy
-rw-r--r-- 2019-01-01 17:04 +0100 1907 Prefix_Order.thy
-rw-r--r-- 2019-01-01 17:04 +0100 1695 Preorder.thy
-rw-r--r-- 2019-01-01 17:04 +0100 3359 Product_Lexorder.thy
-rw-r--r-- 2019-01-01 17:04 +0100 9634 Product_Order.thy
-rw-r--r-- 2019-01-01 17:04 +0100 3372 Product_Plus.thy
-rw-r--r-- 2019-01-01 17:04 +0100 6969 Quadratic_Discriminant.thy
-rw-r--r-- 2019-01-01 17:04 +0100 6834 Quotient_List.thy
-rw-r--r-- 2019-01-01 17:04 +0100 2477 Quotient_Option.thy
-rw-r--r-- 2019-01-01 17:04 +0100 3680 Quotient_Product.thy
-rw-r--r-- 2019-01-01 17:04 +0100 3592 Quotient_Set.thy
-rw-r--r-- 2019-01-01 17:04 +0100 2907 Quotient_Sum.thy
-rw-r--r-- 2019-01-01 17:04 +0100 318 Quotient_Syntax.thy
-rw-r--r-- 2019-01-01 17:04 +0100 6915 Quotient_Type.thy
-rw-r--r-- 2019-01-01 17:04 +0100 8564 RBT.thy
-rw-r--r-- 2019-01-01 17:04 +0100 97670 RBT_Impl.thy
-rw-r--r-- 2019-01-01 17:04 +0100 6568 RBT_Mapping.thy
-rw-r--r-- 2019-01-01 17:04 +0100 28753 RBT_Set.thy
-rw-r--r-- 2019-01-01 17:04 +0100 2666 README.html
-rw-r--r-- 2019-01-01 17:04 +0100 18165 Ramsey.thy
-rw-r--r-- 2019-01-01 17:04 +0100 349 Realizers.thy
-rw-r--r-- 2019-01-01 17:04 +0100 1131 Reflection.thy
-rw-r--r-- 2019-01-01 17:04 +0100 6529 Refute.thy
-rw-r--r-- 2019-01-01 17:04 +0100 1189 Rewrite.thy
-rw-r--r-- 2019-01-01 17:04 +0100 7255 Saturated.thy
-rw-r--r-- 2019-01-01 17:04 +0100 13793 Set_Algebras.thy
-rw-r--r-- 2019-01-01 17:04 +0100 24335 Set_Idioms.thy
-rw-r--r-- 2019-01-01 17:04 +0100 273 Simps_Case_Conv.thy
-rw-r--r-- 2019-01-01 17:04 +0100 22410 Sorting_Algorithms.thy
-rw-r--r-- 2019-01-01 17:04 +0100 8344 State_Monad.thy
-rw-r--r-- 2019-01-01 17:04 +0100 10410 Stirling.thy
-rw-r--r-- 2019-01-01 17:04 +0100 22815 Stream.thy
-rw-r--r-- 2019-01-01 17:04 +0100 52708 Sublist.thy
-rw-r--r-- 2019-01-01 17:04 +0100 2952 Subseq_Order.thy
-rw-r--r-- 2019-01-01 17:04 +0100 535 Sum_of_Squares.thy
-rw-r--r-- 2019-01-01 17:04 +0100 8225 Transitive_Closure_Table.thy
-rw-r--r-- 2019-01-01 17:04 +0100 15328 Tree.thy
-rw-r--r-- 2019-01-01 17:04 +0100 1672 Tree_Multiset.thy
-rw-r--r-- 2019-01-01 17:04 +0100 4223 Tree_Real.thy
-rw-r--r-- 2019-01-01 17:04 +0100 1723 Type_Length.thy
-rw-r--r-- 2019-01-01 17:04 +0100 9175 Uprod.thy
-rw-r--r-- 2019-01-01 17:04 +0100 18271 While_Combinator.thy
-rw-r--r-- 2019-01-01 17:04 +0100 8315 adhoc_overloading.ML
-rw-r--r-- 2019-01-01 17:04 +0100 21680 case_converter.ML
-rw-r--r-- 2019-01-01 17:04 +0100 8448 cconv.ML
-rw-r--r-- 2019-01-01 17:04 +0100 24698 code_lazy.ML
-rw-r--r-- 2019-01-01 17:04 +0100 21304 code_test.ML
-rw-r--r-- 2019-01-01 17:04 +0100 19966 conditional_parametricity.ML
-rw-r--r-- 2019-01-01 17:04 +0100 11354 datatype_records.ML
-rw-r--r-- 2019-01-01 17:04 +0100 1233 multiset_simprocs.ML
-rw-r--r-- 2019-01-01 17:04 +0100 110400 old_recdef.ML
-rw-r--r-- 2019-01-01 17:04 +0100 35396 positivstellensatz.ML
-rw-r--r-- 2019-01-01 17:04 +0100 145229 refute.ML
-rw-r--r-- 2019-01-01 17:04 +0100 16992 rewrite.ML
-rw-r--r-- 2019-01-01 17:04 +0100 4616 simps_case_conv.ML