NameDateSize

..30-Oct-2020171

adhoc_overloading.MLH A D25-Jul-20198.2 KiB

Adhoc_Overloading.thyH A D25-Jul-2019399

AList.thyH A D25-Jul-201927.4 KiB

AList_Mapping.thyH A D25-Jul-20194.3 KiB

BigO.thyH A D25-Jul-201928.8 KiB

BNF_Axiomatization.thyH A D25-Jul-2019400

BNF_Corec.thyH A D25-Jul-20198.6 KiB

Boolean_Algebra.thyH A D30-Oct-202012.3 KiB

Bourbaki_Witt_Fixpoint.thyH A D25-Jul-201916.5 KiB

Cancellation/H30-Oct-20205

Cancellation.thyH A D25-Jul-20194 KiB

Cardinality.thyH A D30-Oct-202020.2 KiB

case_converter.MLH A D25-Jul-201921.2 KiB

Case_Converter.thyH A D25-Jul-2019684

cconv.MLH A D25-Jul-20198.3 KiB

Char_ord.thyH A D25-Jul-20191.4 KiB

Code_Abstract_Nat.thyH A D25-Jul-20193.7 KiB

Code_Binary_Nat.thyH A D25-Jul-20194.6 KiB

code_lazy.MLH A D25-Jul-201924.5 KiB

Code_Lazy.thyH A D25-Jul-20198.7 KiB

Code_Prolog.thyH A D25-Jul-2019537

Code_Real_Approx_By_Float.thyH A D30-Oct-20205.8 KiB

Code_Target_Int.thyH A D25-Jul-20194 KiB

Code_Target_Nat.thyH A D25-Jul-20195.4 KiB

Code_Target_Numeral.thyH A D25-Jul-2019278

code_test.MLH A D30-Oct-202021.3 KiB

Code_Test.thyH A D25-Jul-20195.8 KiB

Combine_PER.thyH A D25-Jul-20192 KiB

Comparator.thyH A D25-Jul-20199.1 KiB

Complete_Partial_Order2.thyH A D30-Oct-202076.4 KiB

conditional_parametricity.MLH A D25-Jul-201919.8 KiB

Conditional_Parametricity.thyH A D25-Jul-20191.5 KiB

Confluence.thyH A D30-Oct-20204.2 KiB

Confluent_Quotient.thyH A D30-Oct-20204.2 KiB

Countable.thyH A D25-Jul-201910.4 KiB

Countable_Complete_Lattices.thyH A D25-Jul-201912.7 KiB

Countable_Set.thyH A D25-Jul-201918.7 KiB

Countable_Set_Type.thyH A D25-Jul-201929 KiB

DAList.thyH A D25-Jul-20196.9 KiB

DAList_Multiset.thyH A D25-Jul-201915.8 KiB

datatype_records.MLH A D30-Oct-202011.2 KiB

Datatype_Records.thyH A D25-Jul-20194 KiB

Debug.thyH A D25-Jul-20191.2 KiB

Diagonal_Subsequence.thyH A D25-Jul-20194 KiB

Discrete.thyH A D30-Oct-202012.5 KiB

Disjoint_Sets.thyH A D25-Jul-201916.7 KiB

Dlist.thyH A D30-Oct-202011.4 KiB

document/H25-Jul-20194

Dual_Ordered_Lattice.thyH A D25-Jul-20198.9 KiB

Equipollence.thyH A D30-Oct-202028.7 KiB

Extended.thyH A D25-Jul-20195 KiB

Extended_Nat.thyH A D25-Jul-201923.2 KiB

Extended_Nonnegative_Real.thyH A D30-Oct-202085.1 KiB

Extended_Real.thyH A D30-Oct-2020162.1 KiB

Finite_Lattice.thyH A D25-Jul-201910.7 KiB

Finite_Map.thyH A D30-Oct-202051.1 KiB

Float.thyH A D30-Oct-202094.4 KiB

FSet.thyH A D25-Jul-201953.6 KiB

Fun_Lexorder.thyH A D25-Jul-20193.5 KiB

FuncSet.thyH A D30-Oct-202028 KiB

Function_Algebras.thyH A D25-Jul-20196.1 KiB

Function_Division.thyH A D25-Jul-20191.7 KiB

Going_To_Filter.thyH A D25-Jul-20196.1 KiB

Groups_Big_Fun.thyH A D25-Jul-201912.5 KiB

IArray.thyH A D25-Jul-20197.7 KiB

Indicator_Function.thyH A D30-Oct-20208.6 KiB

Infinite_Set.thyH A D25-Jul-201915.8 KiB

Interval.thyH A D30-Oct-202032.5 KiB

Interval_Float.thyH A D30-Oct-202013.9 KiB

Landau_Symbols.thyH A D30-Oct-2020102.6 KiB

LaTeXsugar.thyH A D25-Jul-20195.6 KiB

Lattice_Algebras.thyH A D25-Jul-201918.2 KiB

Lattice_Constructions.thyH A D25-Jul-201913.4 KiB

Lattice_Syntax.thyH A D25-Jul-2019815

Library.thyH A D30-Oct-20201.5 KiB

Liminf_Limsup.thyH A D30-Oct-202026.6 KiB

Linear_Temporal_Logic_on_Streams.thyH A D30-Oct-202031.5 KiB

List_Lexorder.thyH A D25-Jul-20193.2 KiB

ListVector.thyH A D25-Jul-20194 KiB

Log_Nat.thyH A D30-Oct-202010.5 KiB

Lub_Glb.thyH A D25-Jul-201910.2 KiB

Mapping.thyH A D25-Jul-201926.2 KiB

Monad_Syntax.thyH A D30-Oct-20202.2 KiB

More_List.thyH A D30-Oct-202013.7 KiB

Multiset.thyH A D30-Oct-2020142.3 KiB

Multiset_Order.thyH A D25-Jul-201917.1 KiB

Multiset_Permutations.thyH A D25-Jul-201921.8 KiB

multiset_simprocs.MLH A D25-Jul-20191.3 KiB

Nat_Bijection.thyH A D25-Jul-201912.4 KiB

Nonpos_Ints.thyH A D30-Oct-202015.1 KiB

Numeral_Type.thyH A D25-Jul-201918.1 KiB

Old_Datatype.thyH A D25-Jul-201915 KiB

old_recdef.MLH A D30-Oct-2020108.9 KiB

Old_Recdef.thyH A D25-Jul-20192.3 KiB

Omega_Words_Fun.thyH A D25-Jul-201931.5 KiB

Open_State_Syntax.thyH A D25-Jul-20195.5 KiB

Option_ord.thyH A D25-Jul-201919 KiB

OptionalSugar.thyH A D25-Jul-20192.3 KiB

Order_Continuity.thyH A D25-Jul-201918.2 KiB

Parallel.thyH A D25-Jul-20191.6 KiB

Pattern_Aliases.thyH A D25-Jul-20197.5 KiB

Periodic_Fun.thyH A D25-Jul-20195.3 KiB

Perm.thyH A D30-Oct-202025.6 KiB

Permutation.thyH A D30-Oct-20208 KiB

Permutations.thyH A D25-Jul-201954.5 KiB

Phantom_Type.thyH A D25-Jul-20191.2 KiB

Poly_Mapping.thyH A D25-Jul-201967.4 KiB

Power_By_Squaring.thyH A D25-Jul-20192.3 KiB

Predicate_Compile_Alternative_Defs.thyH A D25-Jul-20199.8 KiB

Predicate_Compile_Quickcheck.thyH A D25-Jul-2019365

Prefix_Order.thyH A D25-Jul-20191.9 KiB

Preorder.thyH A D25-Jul-20192.8 KiB

Product_Lexorder.thyH A D25-Jul-20193.3 KiB

Product_Order.thyH A D25-Jul-20199.5 KiB

Product_Plus.thyH A D25-Jul-20193.3 KiB

Quadratic_Discriminant.thyH A D25-Jul-20196.8 KiB

Quantified_Premise_Simproc.thyH A D30-Oct-2020202

Quotient_List.thyH A D25-Jul-20196.7 KiB

Quotient_Option.thyH A D25-Jul-20192.4 KiB

Quotient_Product.thyH A D25-Jul-20193.6 KiB

Quotient_Set.thyH A D25-Jul-20193.5 KiB

Quotient_Sum.thyH A D25-Jul-20192.8 KiB

Quotient_Syntax.thyH A D25-Jul-2019318

Quotient_Type.thyH A D25-Jul-20196.8 KiB

Ramsey.thyH A D30-Oct-202044.1 KiB

RBT.thyH A D25-Jul-20198.4 KiB

RBT_Impl.thyH A D25-Jul-201995.9 KiB

RBT_Mapping.thyH A D25-Jul-20196.5 KiB

RBT_Set.thyH A D25-Jul-201928.1 KiB

README.htmlH A D25-Jul-20192.6 KiB

Realizers.thyH A D25-Jul-2019375

Reflection.thyH A D25-Jul-20191.1 KiB

refute.MLH A D25-Jul-2019144.6 KiB

Refute.thyH A D25-Jul-20196.4 KiB

rewrite.MLH A D25-Jul-201916.7 KiB

Rewrite.thyH A D25-Jul-20191.2 KiB

Saturated.thyH A D25-Jul-20197 KiB

Set_Algebras.thyH A D25-Jul-201913.5 KiB

Set_Idioms.thyH A D25-Jul-201924.2 KiB

simps_case_conv.MLH A D25-Jul-20194.6 KiB

Simps_Case_Conv.thyH A D25-Jul-2019286

Sorting_Algorithms.thyH A D25-Jul-201921.9 KiB

State_Monad.thyH A D25-Jul-20198.1 KiB

Stirling.thyH A D25-Jul-201910.2 KiB

Stream.thyH A D25-Jul-201922.3 KiB

Sublist.thyH A D25-Jul-201951.5 KiB

Subseq_Order.thyH A D25-Jul-20192.9 KiB

Sum_of_Squares/H30-Oct-20206

Sum_of_Squares.thyH A D30-Oct-2020602

Transitive_Closure_Table.thyH A D25-Jul-20198 KiB

Tree.thyH A D25-Jul-201915.1 KiB

Tree_Multiset.thyH A D25-Jul-20191.7 KiB

Tree_Real.thyH A D30-Oct-20204.1 KiB

Type_Length.thyH A D30-Oct-20202.5 KiB

Uprod.thyH A D25-Jul-20199 KiB

While_Combinator.thyH A D25-Jul-201917.9 KiB

Z2.thyH A D30-Oct-20204.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