Name | Date | Size | ||
---|---|---|---|---|
.. | 30-Oct-2020 | 171 | ||
adhoc_overloading.ML | H A D | 25-Jul-2019 | 8.2 KiB | |
Adhoc_Overloading.thy | H A D | 25-Jul-2019 | 399 | |
AList.thy | H A D | 25-Jul-2019 | 27.4 KiB | |
AList_Mapping.thy | H A D | 25-Jul-2019 | 4.3 KiB | |
BigO.thy | H A D | 25-Jul-2019 | 28.8 KiB | |
BNF_Axiomatization.thy | H A D | 25-Jul-2019 | 400 | |
BNF_Corec.thy | H A D | 25-Jul-2019 | 8.6 KiB | |
Boolean_Algebra.thy | H A D | 30-Oct-2020 | 12.3 KiB | |
Bourbaki_Witt_Fixpoint.thy | H A D | 25-Jul-2019 | 16.5 KiB | |
Cancellation/ | H | 30-Oct-2020 | 5 | |
Cancellation.thy | H A D | 25-Jul-2019 | 4 KiB | |
Cardinality.thy | H A D | 30-Oct-2020 | 20.2 KiB | |
case_converter.ML | H A D | 25-Jul-2019 | 21.2 KiB | |
Case_Converter.thy | H A D | 25-Jul-2019 | 684 | |
cconv.ML | H A D | 25-Jul-2019 | 8.3 KiB | |
Char_ord.thy | H A D | 25-Jul-2019 | 1.4 KiB | |
Code_Abstract_Nat.thy | H A D | 25-Jul-2019 | 3.7 KiB | |
Code_Binary_Nat.thy | H A D | 25-Jul-2019 | 4.6 KiB | |
code_lazy.ML | H A D | 25-Jul-2019 | 24.5 KiB | |
Code_Lazy.thy | H A D | 25-Jul-2019 | 8.7 KiB | |
Code_Prolog.thy | H A D | 25-Jul-2019 | 537 | |
Code_Real_Approx_By_Float.thy | H A D | 30-Oct-2020 | 5.8 KiB | |
Code_Target_Int.thy | H A D | 25-Jul-2019 | 4 KiB | |
Code_Target_Nat.thy | H A D | 25-Jul-2019 | 5.4 KiB | |
Code_Target_Numeral.thy | H A D | 25-Jul-2019 | 278 | |
code_test.ML | H A D | 30-Oct-2020 | 21.3 KiB | |
Code_Test.thy | H A D | 25-Jul-2019 | 5.8 KiB | |
Combine_PER.thy | H A D | 25-Jul-2019 | 2 KiB | |
Comparator.thy | H A D | 25-Jul-2019 | 9.1 KiB | |
Complete_Partial_Order2.thy | H A D | 30-Oct-2020 | 76.4 KiB | |
conditional_parametricity.ML | H A D | 25-Jul-2019 | 19.8 KiB | |
Conditional_Parametricity.thy | H A D | 25-Jul-2019 | 1.5 KiB | |
Confluence.thy | H A D | 30-Oct-2020 | 4.2 KiB | |
Confluent_Quotient.thy | H A D | 30-Oct-2020 | 4.2 KiB | |
Countable.thy | H A D | 25-Jul-2019 | 10.4 KiB | |
Countable_Complete_Lattices.thy | H A D | 25-Jul-2019 | 12.7 KiB | |
Countable_Set.thy | H A D | 25-Jul-2019 | 18.7 KiB | |
Countable_Set_Type.thy | H A D | 25-Jul-2019 | 29 KiB | |
DAList.thy | H A D | 25-Jul-2019 | 6.9 KiB | |
DAList_Multiset.thy | H A D | 25-Jul-2019 | 15.8 KiB | |
datatype_records.ML | H A D | 30-Oct-2020 | 11.2 KiB | |
Datatype_Records.thy | H A D | 25-Jul-2019 | 4 KiB | |
Debug.thy | H A D | 25-Jul-2019 | 1.2 KiB | |
Diagonal_Subsequence.thy | H A D | 25-Jul-2019 | 4 KiB | |
Discrete.thy | H A D | 30-Oct-2020 | 12.5 KiB | |
Disjoint_Sets.thy | H A D | 25-Jul-2019 | 16.7 KiB | |
Dlist.thy | H A D | 30-Oct-2020 | 11.4 KiB | |
document/ | H | 25-Jul-2019 | 4 | |
Dual_Ordered_Lattice.thy | H A D | 25-Jul-2019 | 8.9 KiB | |
Equipollence.thy | H A D | 30-Oct-2020 | 28.7 KiB | |
Extended.thy | H A D | 25-Jul-2019 | 5 KiB | |
Extended_Nat.thy | H A D | 25-Jul-2019 | 23.2 KiB | |
Extended_Nonnegative_Real.thy | H A D | 30-Oct-2020 | 85.1 KiB | |
Extended_Real.thy | H A D | 30-Oct-2020 | 162.1 KiB | |
Finite_Lattice.thy | H A D | 25-Jul-2019 | 10.7 KiB | |
Finite_Map.thy | H A D | 30-Oct-2020 | 51.1 KiB | |
Float.thy | H A D | 30-Oct-2020 | 94.4 KiB | |
FSet.thy | H A D | 25-Jul-2019 | 53.6 KiB | |
Fun_Lexorder.thy | H A D | 25-Jul-2019 | 3.5 KiB | |
FuncSet.thy | H A D | 30-Oct-2020 | 28 KiB | |
Function_Algebras.thy | H A D | 25-Jul-2019 | 6.1 KiB | |
Function_Division.thy | H A D | 25-Jul-2019 | 1.7 KiB | |
Going_To_Filter.thy | H A D | 25-Jul-2019 | 6.1 KiB | |
Groups_Big_Fun.thy | H A D | 25-Jul-2019 | 12.5 KiB | |
IArray.thy | H A D | 25-Jul-2019 | 7.7 KiB | |
Indicator_Function.thy | H A D | 30-Oct-2020 | 8.6 KiB | |
Infinite_Set.thy | H A D | 25-Jul-2019 | 15.8 KiB | |
Interval.thy | H A D | 30-Oct-2020 | 32.5 KiB | |
Interval_Float.thy | H A D | 30-Oct-2020 | 13.9 KiB | |
Landau_Symbols.thy | H A D | 30-Oct-2020 | 102.6 KiB | |
LaTeXsugar.thy | H A D | 25-Jul-2019 | 5.6 KiB | |
Lattice_Algebras.thy | H A D | 25-Jul-2019 | 18.2 KiB | |
Lattice_Constructions.thy | H A D | 25-Jul-2019 | 13.4 KiB | |
Lattice_Syntax.thy | H A D | 25-Jul-2019 | 815 | |
Library.thy | H A D | 30-Oct-2020 | 1.5 KiB | |
Liminf_Limsup.thy | H A D | 30-Oct-2020 | 26.6 KiB | |
Linear_Temporal_Logic_on_Streams.thy | H A D | 30-Oct-2020 | 31.5 KiB | |
List_Lexorder.thy | H A D | 25-Jul-2019 | 3.2 KiB | |
ListVector.thy | H A D | 25-Jul-2019 | 4 KiB | |
Log_Nat.thy | H A D | 30-Oct-2020 | 10.5 KiB | |
Lub_Glb.thy | H A D | 25-Jul-2019 | 10.2 KiB | |
Mapping.thy | H A D | 25-Jul-2019 | 26.2 KiB | |
Monad_Syntax.thy | H A D | 30-Oct-2020 | 2.2 KiB | |
More_List.thy | H A D | 30-Oct-2020 | 13.7 KiB | |
Multiset.thy | H A D | 30-Oct-2020 | 142.3 KiB | |
Multiset_Order.thy | H A D | 25-Jul-2019 | 17.1 KiB | |
Multiset_Permutations.thy | H A D | 25-Jul-2019 | 21.8 KiB | |
multiset_simprocs.ML | H A D | 25-Jul-2019 | 1.3 KiB | |
Nat_Bijection.thy | H A D | 25-Jul-2019 | 12.4 KiB | |
Nonpos_Ints.thy | H A D | 30-Oct-2020 | 15.1 KiB | |
Numeral_Type.thy | H A D | 25-Jul-2019 | 18.1 KiB | |
Old_Datatype.thy | H A D | 25-Jul-2019 | 15 KiB | |
old_recdef.ML | H A D | 30-Oct-2020 | 108.9 KiB | |
Old_Recdef.thy | H A D | 25-Jul-2019 | 2.3 KiB | |
Omega_Words_Fun.thy | H A D | 25-Jul-2019 | 31.5 KiB | |
Open_State_Syntax.thy | H A D | 25-Jul-2019 | 5.5 KiB | |
Option_ord.thy | H A D | 25-Jul-2019 | 19 KiB | |
OptionalSugar.thy | H A D | 25-Jul-2019 | 2.3 KiB | |
Order_Continuity.thy | H A D | 25-Jul-2019 | 18.2 KiB | |
Parallel.thy | H A D | 25-Jul-2019 | 1.6 KiB | |
Pattern_Aliases.thy | H A D | 25-Jul-2019 | 7.5 KiB | |
Periodic_Fun.thy | H A D | 25-Jul-2019 | 5.3 KiB | |
Perm.thy | H A D | 30-Oct-2020 | 25.6 KiB | |
Permutation.thy | H A D | 30-Oct-2020 | 8 KiB | |
Permutations.thy | H A D | 25-Jul-2019 | 54.5 KiB | |
Phantom_Type.thy | H A D | 25-Jul-2019 | 1.2 KiB | |
Poly_Mapping.thy | H A D | 25-Jul-2019 | 67.4 KiB | |
Power_By_Squaring.thy | H A D | 25-Jul-2019 | 2.3 KiB | |
Predicate_Compile_Alternative_Defs.thy | H A D | 25-Jul-2019 | 9.8 KiB | |
Predicate_Compile_Quickcheck.thy | H A D | 25-Jul-2019 | 365 | |
Prefix_Order.thy | H A D | 25-Jul-2019 | 1.9 KiB | |
Preorder.thy | H A D | 25-Jul-2019 | 2.8 KiB | |
Product_Lexorder.thy | H A D | 25-Jul-2019 | 3.3 KiB | |
Product_Order.thy | H A D | 25-Jul-2019 | 9.5 KiB | |
Product_Plus.thy | H A D | 25-Jul-2019 | 3.3 KiB | |
Quadratic_Discriminant.thy | H A D | 25-Jul-2019 | 6.8 KiB | |
Quantified_Premise_Simproc.thy | H A D | 30-Oct-2020 | 202 | |
Quotient_List.thy | H A D | 25-Jul-2019 | 6.7 KiB | |
Quotient_Option.thy | H A D | 25-Jul-2019 | 2.4 KiB | |
Quotient_Product.thy | H A D | 25-Jul-2019 | 3.6 KiB | |
Quotient_Set.thy | H A D | 25-Jul-2019 | 3.5 KiB | |
Quotient_Sum.thy | H A D | 25-Jul-2019 | 2.8 KiB | |
Quotient_Syntax.thy | H A D | 25-Jul-2019 | 318 | |
Quotient_Type.thy | H A D | 25-Jul-2019 | 6.8 KiB | |
Ramsey.thy | H A D | 30-Oct-2020 | 44.1 KiB | |
RBT.thy | H A D | 25-Jul-2019 | 8.4 KiB | |
RBT_Impl.thy | H A D | 25-Jul-2019 | 95.9 KiB | |
RBT_Mapping.thy | H A D | 25-Jul-2019 | 6.5 KiB | |
RBT_Set.thy | H A D | 25-Jul-2019 | 28.1 KiB | |
README.html | H A D | 25-Jul-2019 | 2.6 KiB | |
Realizers.thy | H A D | 25-Jul-2019 | 375 | |
Reflection.thy | H A D | 25-Jul-2019 | 1.1 KiB | |
refute.ML | H A D | 25-Jul-2019 | 144.6 KiB | |
Refute.thy | H A D | 25-Jul-2019 | 6.4 KiB | |
rewrite.ML | H A D | 25-Jul-2019 | 16.7 KiB | |
Rewrite.thy | H A D | 25-Jul-2019 | 1.2 KiB | |
Saturated.thy | H A D | 25-Jul-2019 | 7 KiB | |
Set_Algebras.thy | H A D | 25-Jul-2019 | 13.5 KiB | |
Set_Idioms.thy | H A D | 25-Jul-2019 | 24.2 KiB | |
simps_case_conv.ML | H A D | 25-Jul-2019 | 4.6 KiB | |
Simps_Case_Conv.thy | H A D | 25-Jul-2019 | 286 | |
Sorting_Algorithms.thy | H A D | 25-Jul-2019 | 21.9 KiB | |
State_Monad.thy | H A D | 25-Jul-2019 | 8.1 KiB | |
Stirling.thy | H A D | 25-Jul-2019 | 10.2 KiB | |
Stream.thy | H A D | 25-Jul-2019 | 22.3 KiB | |
Sublist.thy | H A D | 25-Jul-2019 | 51.5 KiB | |
Subseq_Order.thy | H A D | 25-Jul-2019 | 2.9 KiB | |
Sum_of_Squares/ | H | 30-Oct-2020 | 6 | |
Sum_of_Squares.thy | H A D | 30-Oct-2020 | 602 | |
Transitive_Closure_Table.thy | H A D | 25-Jul-2019 | 8 KiB | |
Tree.thy | H A D | 25-Jul-2019 | 15.1 KiB | |
Tree_Multiset.thy | H A D | 25-Jul-2019 | 1.7 KiB | |
Tree_Real.thy | H A D | 30-Oct-2020 | 4.1 KiB | |
Type_Length.thy | H A D | 30-Oct-2020 | 2.5 KiB | |
Uprod.thy | H A D | 25-Jul-2019 | 9 KiB | |
While_Combinator.thy | H A D | 25-Jul-2019 | 17.9 KiB | |
Z2.thy | H A D | 30-Oct-2020 | 4.6 KiB |
README.html
1<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> 2 3<html> 4 5<head> 6 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> 7 <title>HOL-Library/README</title> 8</head> 9 10<body> 11 12<h1>HOL-Library: supplemental theories for main Isabelle/HOL</h1> 13 14This is a collection of generic theories that may be used together 15with main Isabelle/HOL. 16 17<p> 18 19Addition of new theories should be done with some care, as the 20``module system'' of Isabelle is rather simplistic. The following 21guidelines may be helpful to achieve maximum re-usability and minimum 22clashes with existing developments. 23 24<dl> 25 26<dt><strong>Examples</strong> 27 28<dd>Theories should be as ``generic'' as is sensible. Unused (or 29rather unusable?) theories should be avoided; common applications 30should actually refer to the present theory. Small example uses may 31be included in the library as well, but should be put in a separate 32theory, such as <tt>Foobar</tt> accompanied by 33<tt>Foobar_Examples</tt>. 34 35<dt><strong>Theory names</strong> 36 37<dd>The theory loader name space is <em>flat</em>, so use sufficiently 38long and descriptive names to reduce the danger of clashes with the 39user's own theories. The convention for theory names is as follows: 40<tt>Foobar_Doobar</tt> (this looks best in LaTeX output). 41 42<dt><strong>Names of logical items</strong> 43 44<dd>There are separate hierarchically structured name spaces for 45types, constants, theorems etc. Nevertheless, some care should be 46taken, as the name spaces are always ``open''. Use adequate names; 47avoid unreadable abbreviations. The general naming convention is to 48separate word constituents by underscores, as in <tt>foo_bar</tt> or 49<tt>Foo_Bar</tt> (this looks best in LaTeX output). 50 51<dt><strong>Global context declarations</strong> 52 53<dd>Only items introduced in the present theory should be declared 54globally (e.g. as Simplifier rules). Note that adding and deleting 55rules from parent theories may result in strange behavior later, 56depending on the user's arrangement of import lists. 57 58<dt><strong>Spacing</strong> 59 60<dd>Isabelle is able to produce a high-quality LaTeX document from the 61theory sources, provided some minor issues are taken care of. In 62particular, spacing and line breaks are directly taken from source 63text. Incidentally, output looks very good if common type-setting 64conventions are observed: put a single space <em>after</em> each 65punctuation character ("<tt>,</tt>", "<tt>.</tt>", etc.), but none 66before it; do not extra spaces inside of parentheses; do not attempt 67to simulate table markup with spaces, avoid ``hanging'' indentations. 68 69</dl> 70 71</body> 72</html> 73