/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-03-22 19:18 +0000 28031 AList.thy
-rw-r--r-- 2019-03-22 19:18 +0000 4392 AList_Mapping.thy
-rw-r--r-- 2019-03-22 19:18 +0000 399 Adhoc_Overloading.thy
-rw-r--r-- 2019-03-22 19:18 +0000 400 BNF_Axiomatization.thy
-rw-r--r-- 2019-03-22 19:18 +0000 8771 BNF_Corec.thy
-rw-r--r-- 2019-03-22 19:18 +0000 29440 BigO.thy
-rw-r--r-- 2019-03-22 19:18 +0000 4471 Bit.thy
-rw-r--r-- 2019-03-22 19:18 +0000 11537 Boolean_Algebra.thy
-rw-r--r-- 2019-03-22 19:18 +0000 16882 Bourbaki_Witt_Fixpoint.thy
-rw-r--r-- 2019-03-22 19:18 +0000 4072 Cancellation.thy
-rw-r--r-- 2019-03-22 19:18 +0000 793 Cardinal_Notations.thy
-rw-r--r-- 2019-03-22 19:18 +0000 20752 Cardinality.thy
-rw-r--r-- 2019-03-22 19:18 +0000 684 Case_Converter.thy
-rw-r--r-- 2019-03-22 19:18 +0000 1473 Char_ord.thy
-rw-r--r-- 2019-03-22 19:18 +0000 3812 Code_Abstract_Nat.thy
-rw-r--r-- 2019-03-22 19:18 +0000 4710 Code_Binary_Nat.thy
-rw-r--r-- 2019-03-22 19:18 +0000 8946 Code_Lazy.thy
-rw-r--r-- 2019-03-22 19:18 +0000 537 Code_Prolog.thy
-rw-r--r-- 2019-03-22 19:18 +0000 5844 Code_Real_Approx_By_Float.thy
-rw-r--r-- 2019-03-22 19:18 +0000 4049 Code_Target_Int.thy
-rw-r--r-- 2019-03-22 19:18 +0000 5552 Code_Target_Nat.thy
-rw-r--r-- 2019-03-22 19:18 +0000 278 Code_Target_Numeral.thy
-rw-r--r-- 2019-03-22 19:18 +0000 5901 Code_Test.thy
-rw-r--r-- 2019-03-22 19:18 +0000 2097 Combine_PER.thy
-rw-r--r-- 2019-03-22 19:18 +0000 9338 Comparator.thy
-rw-r--r-- 2019-03-22 19:18 +0000 78332 Complete_Partial_Order2.thy
-rw-r--r-- 2019-03-22 19:18 +0000 1506 Conditional_Parametricity.thy
-rw-r--r-- 2019-03-22 19:18 +0000 10684 Countable.thy
-rw-r--r-- 2019-03-22 19:18 +0000 13024 Countable_Complete_Lattices.thy
-rw-r--r-- 2019-03-22 19:18 +0000 16398 Countable_Set.thy
-rw-r--r-- 2019-03-22 19:18 +0000 29598 Countable_Set_Type.thy
-rw-r--r-- 2019-03-22 19:18 +0000 7085 DAList.thy
-rw-r--r-- 2019-03-22 19:18 +0000 16187 DAList_Multiset.thy
-rw-r--r-- 2019-03-22 19:18 +0000 4081 Datatype_Records.thy
-rw-r--r-- 2019-03-22 19:18 +0000 1226 Debug.thy
-rw-r--r-- 2019-03-22 19:18 +0000 4063 Diagonal_Subsequence.thy
-rw-r--r-- 2019-03-22 19:18 +0000 12748 Discrete.thy
-rw-r--r-- 2019-03-22 19:18 +0000 17117 Disjoint_Sets.thy
-rw-r--r-- 2019-03-22 19:18 +0000 12694 Dlist.thy
-rw-r--r-- 2019-03-22 19:18 +0000 8926 Dual_Ordered_Lattice.thy
-rw-r--r-- 2019-03-22 19:18 +0000 14853 Equipollence.thy
-rw-r--r-- 2019-03-22 19:18 +0000 5170 Extended.thy
-rw-r--r-- 2019-03-22 19:18 +0000 23781 Extended_Nat.thy
-rw-r--r-- 2019-03-22 19:18 +0000 85871 Extended_Nonnegative_Real.thy
-rw-r--r-- 2019-03-22 19:18 +0000 164818 Extended_Real.thy
-rw-r--r-- 2019-03-22 19:18 +0000 54874 FSet.thy
-rw-r--r-- 2019-03-22 19:18 +0000 10971 Finite_Lattice.thy
-rw-r--r-- 2019-03-22 19:18 +0000 51759 Finite_Map.thy
-rw-r--r-- 2019-03-22 19:18 +0000 85816 Float.thy
-rw-r--r-- 2019-03-22 19:18 +0000 3578 Fun_Lexorder.thy
-rw-r--r-- 2019-03-22 19:18 +0000 28434 FuncSet.thy
-rw-r--r-- 2019-03-22 19:18 +0000 6290 Function_Algebras.thy
-rw-r--r-- 2019-03-22 19:18 +0000 1765 Function_Division.thy
-rw-r--r-- 2019-03-22 19:18 +0000 6234 Going_To_Filter.thy
-rw-r--r-- 2019-03-22 19:18 +0000 12839 Groups_Big_Fun.thy
-rw-r--r-- 2019-03-22 19:18 +0000 7866 IArray.thy
-rw-r--r-- 2019-03-22 19:18 +0000 8467 Indicator_Function.thy
-rw-r--r-- 2019-03-22 19:18 +0000 16199 Infinite_Set.thy
-rw-r--r-- 2019-03-22 19:18 +0000 5720 LaTeXsugar.thy
-rw-r--r-- 2019-03-22 19:18 +0000 105233 Landau_Symbols.thy
-rw-r--r-- 2019-03-22 19:18 +0000 18608 Lattice_Algebras.thy
-rw-r--r-- 2019-03-22 19:18 +0000 13708 Lattice_Constructions.thy
-rw-r--r-- 2019-03-22 19:18 +0000 815 Lattice_Syntax.thy
-rw-r--r-- 2019-03-22 19:18 +0000 1485 Library.thy
-rw-r--r-- 2019-03-22 19:18 +0000 26857 Liminf_Limsup.thy
-rw-r--r-- 2019-03-22 19:18 +0000 28762 Linear_Temporal_Logic_on_Streams.thy
-rw-r--r-- 2019-03-22 19:18 +0000 4109 ListVector.thy
-rw-r--r-- 2019-03-22 19:18 +0000 3256 List_Lexorder.thy
-rw-r--r-- 2019-03-22 19:18 +0000 10832 Log_Nat.thy
-rw-r--r-- 2019-03-22 19:18 +0000 10402 Lub_Glb.thy
-rw-r--r-- 2019-03-22 19:18 +0000 26841 Mapping.thy
-rw-r--r-- 2019-03-22 19:18 +0000 2236 Monad_Syntax.thy
-rw-r--r-- 2019-03-22 19:18 +0000 13618 More_List.thy
-rw-r--r-- 2019-03-22 19:18 +0000 145286 Multiset.thy
-rw-r--r-- 2019-03-22 19:18 +0000 17499 Multiset_Order.thy
-rw-r--r-- 2019-03-22 19:18 +0000 22276 Multiset_Permutations.thy
-rw-r--r-- 2019-03-22 19:18 +0000 12703 Nat_Bijection.thy
-rw-r--r-- 2019-03-22 19:18 +0000 15435 Nonpos_Ints.thy
-rw-r--r-- 2019-03-22 19:18 +0000 18581 Numeral_Type.thy
-rw-r--r-- 2019-03-22 19:18 +0000 15329 Old_Datatype.thy
-rw-r--r-- 2019-03-22 19:18 +0000 2385 Old_Recdef.thy
-rw-r--r-- 2019-03-22 19:18 +0000 32207 Omega_Words_Fun.thy
-rw-r--r-- 2019-03-22 19:18 +0000 5593 Open_State_Syntax.thy
-rw-r--r-- 2019-03-22 19:18 +0000 19474 Option_ord.thy
-rw-r--r-- 2019-03-22 19:18 +0000 2313 OptionalSugar.thy
-rw-r--r-- 2019-03-22 19:18 +0000 18615 Order_Continuity.thy
-rw-r--r-- 2019-03-22 19:18 +0000 1618 Parallel.thy
-rw-r--r-- 2019-03-22 19:18 +0000 7662 Pattern_Aliases.thy
-rw-r--r-- 2019-03-22 19:18 +0000 5466 Periodic_Fun.thy
-rw-r--r-- 2019-03-22 19:18 +0000 26289 Perm.thy
-rw-r--r-- 2019-03-22 19:18 +0000 9384 Permutation.thy
-rw-r--r-- 2019-03-22 19:18 +0000 55823 Permutations.thy
-rw-r--r-- 2019-03-22 19:18 +0000 1236 Phantom_Type.thy
-rw-r--r-- 2019-03-22 19:18 +0000 2345 Power_By_Squaring.thy
-rw-r--r-- 2019-03-22 19:18 +0000 10047 Predicate_Compile_Alternative_Defs.thy
-rw-r--r-- 2019-03-22 19:18 +0000 365 Predicate_Compile_Quickcheck.thy
-rw-r--r-- 2019-03-22 19:18 +0000 1907 Prefix_Order.thy
-rw-r--r-- 2019-03-22 19:18 +0000 2822 Preorder.thy
-rw-r--r-- 2019-03-22 19:18 +0000 3359 Product_Lexorder.thy
-rw-r--r-- 2019-03-22 19:18 +0000 9701 Product_Order.thy
-rw-r--r-- 2019-03-22 19:18 +0000 3372 Product_Plus.thy
-rw-r--r-- 2019-03-22 19:18 +0000 6969 Quadratic_Discriminant.thy
-rw-r--r-- 2019-03-22 19:18 +0000 6834 Quotient_List.thy
-rw-r--r-- 2019-03-22 19:18 +0000 2477 Quotient_Option.thy
-rw-r--r-- 2019-03-22 19:18 +0000 3680 Quotient_Product.thy
-rw-r--r-- 2019-03-22 19:18 +0000 3592 Quotient_Set.thy
-rw-r--r-- 2019-03-22 19:18 +0000 2907 Quotient_Sum.thy
-rw-r--r-- 2019-03-22 19:18 +0000 318 Quotient_Syntax.thy
-rw-r--r-- 2019-03-22 19:18 +0000 6930 Quotient_Type.thy
-rw-r--r-- 2019-03-22 19:18 +0000 8564 RBT.thy
-rw-r--r-- 2019-03-22 19:18 +0000 98204 RBT_Impl.thy
-rw-r--r-- 2019-03-22 19:18 +0000 6672 RBT_Mapping.thy
-rw-r--r-- 2019-03-22 19:18 +0000 28753 RBT_Set.thy
-rw-r--r-- 2019-03-22 19:18 +0000 2666 README.html
-rw-r--r-- 2019-03-22 19:18 +0000 18245 Ramsey.thy
-rw-r--r-- 2019-03-22 19:18 +0000 375 Realizers.thy
-rw-r--r-- 2019-03-22 19:18 +0000 1144 Reflection.thy
-rw-r--r-- 2019-03-22 19:18 +0000 6542 Refute.thy
-rw-r--r-- 2019-03-22 19:18 +0000 1215 Rewrite.thy
-rw-r--r-- 2019-03-22 19:18 +0000 7255 Saturated.thy
-rw-r--r-- 2019-03-22 19:18 +0000 13793 Set_Algebras.thy
-rw-r--r-- 2019-03-22 19:18 +0000 24735 Set_Idioms.thy
-rw-r--r-- 2019-03-22 19:18 +0000 286 Simps_Case_Conv.thy
-rw-r--r-- 2019-03-22 19:18 +0000 22410 Sorting_Algorithms.thy
-rw-r--r-- 2019-03-22 19:18 +0000 8344 State_Monad.thy
-rw-r--r-- 2019-03-22 19:18 +0000 10410 Stirling.thy
-rw-r--r-- 2019-03-22 19:18 +0000 22854 Stream.thy
-rw-r--r-- 2019-03-22 19:18 +0000 52708 Sublist.thy
-rw-r--r-- 2019-03-22 19:18 +0000 2952 Subseq_Order.thy
-rw-r--r-- 2019-03-22 19:18 +0000 587 Sum_of_Squares.thy
-rw-r--r-- 2019-03-22 19:18 +0000 8225 Transitive_Closure_Table.thy
-rw-r--r-- 2019-03-22 19:18 +0000 15507 Tree.thy
-rw-r--r-- 2019-03-22 19:18 +0000 1735 Tree_Multiset.thy
-rw-r--r-- 2019-03-22 19:18 +0000 4266 Tree_Real.thy
-rw-r--r-- 2019-03-22 19:18 +0000 1779 Type_Length.thy
-rw-r--r-- 2019-03-22 19:18 +0000 9175 Uprod.thy
-rw-r--r-- 2019-03-22 19:18 +0000 18301 While_Combinator.thy
-rw-r--r-- 2019-03-22 19:18 +0000 8360 adhoc_overloading.ML
-rw-r--r-- 2019-03-22 19:18 +0000 21695 case_converter.ML
-rw-r--r-- 2019-03-22 19:18 +0000 8513 cconv.ML
-rw-r--r-- 2019-03-22 19:18 +0000 25091 code_lazy.ML
-rw-r--r-- 2019-03-22 19:18 +0000 21755 code_test.ML
-rw-r--r-- 2019-03-22 19:18 +0000 20294 conditional_parametricity.ML
-rw-r--r-- 2019-03-22 19:18 +0000 11416 datatype_records.ML
-rw-r--r-- 2019-03-22 19:18 +0000 1293 multiset_simprocs.ML
-rw-r--r-- 2019-03-22 19:18 +0000 111457 old_recdef.ML
-rw-r--r-- 2019-03-22 19:18 +0000 35397 positivstellensatz.ML
-rw-r--r-- 2019-03-22 19:18 +0000 148118 refute.ML
-rw-r--r-- 2019-03-22 19:18 +0000 17128 rewrite.ML
-rw-r--r-- 2019-03-22 19:18 +0000 4700 simps_case_conv.ML