NameDateSize

..25-Jul-2019169

adhoc_overloading.MLH A D25-Jul-20198.1 KiB

Adhoc_Overloading.thyH A D25-Jul-2019386

AList.thyH A D25-Jul-201927.3 KiB

AList_Mapping.thyH A D25-Jul-20194.3 KiB

BigO.thyH A D25-Jul-201928.8 KiB

Bit.thyH A D25-Jul-20194.3 KiB

BNF_Axiomatization.thyH A D25-Jul-2019387

BNF_Corec.thyH A D25-Jul-20198.5 KiB

Boolean_Algebra.thyH A D25-Jul-201911.3 KiB

Bourbaki_Witt_Fixpoint.thyH A D25-Jul-201916.5 KiB

Cancellation/H25-Jul-20195

Cancellation.thyH A D25-Jul-20193.9 KiB

Cardinal_Notations.thyH A D25-Jul-2019793

Cardinality.thyH A D25-Jul-201919.9 KiB

case_converter.MLH A D25-Jul-201919.4 KiB

cconv.MLH A D25-Jul-20198.2 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 KiB

Code_Lazy.thyH A D25-Jul-20199 KiB

Code_Prolog.thyH A D25-Jul-2019494

Code_Real_Approx_By_Float.thyH A D25-Jul-20195.7 KiB

Code_Target_Int.thyH A D25-Jul-20194 KiB

Code_Target_Nat.thyH A D25-Jul-20194.9 KiB

Code_Target_Numeral.thyH A D25-Jul-2019278

code_test.MLH A D25-Jul-201920.8 KiB

Code_Test.thyH A D25-Jul-20195.7 KiB

Combine_PER.thyH A D25-Jul-20192 KiB

Complete_Partial_Order2.thyH A D25-Jul-201976.4 KiB

conditional_parametricity.MLH A D25-Jul-201919.5 KiB

Conditional_Parametricity.thyH A D25-Jul-20191.5 KiB

Countable.thyH A D25-Jul-201910.4 KiB

Countable_Complete_Lattices.thyH A D25-Jul-201912.4 KiB

Countable_Set.thyH A D25-Jul-201916 KiB

Countable_Set_Type.thyH A D25-Jul-201929.1 KiB

DAList.thyH A D25-Jul-20196.9 KiB

DAList_Multiset.thyH A D25-Jul-201915.8 KiB

datatype_records.MLH A D25-Jul-20196.5 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 D25-Jul-201912.5 KiB

Disjoint_Sets.thyH A D25-Jul-201915.3 KiB

Dlist.thyH A D25-Jul-201912.4 KiB

document/H25-Jul-20194

Extended.thyH A D25-Jul-20195 KiB

Extended_Nat.thyH A D25-Jul-201922.6 KiB

Extended_Nonnegative_Real.thyH A D25-Jul-201983.2 KiB

Extended_Real.thyH A D25-Jul-2019159.7 KiB

Finite_Lattice.thyH A D25-Jul-201910.2 KiB

Finite_Map.thyH A D25-Jul-201941.7 KiB

Float.thyH A D25-Jul-201983.8 KiB

FSet.thyH A D25-Jul-201953.5 KiB

Fun_Lexorder.thyH A D25-Jul-20193.5 KiB

FuncSet.thyH A D25-Jul-201923.3 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 KiB

Groups_Big_Fun.thyH A D25-Jul-201912.7 KiB

IArray.thyH A D25-Jul-20197.5 KiB

Indicator_Function.thyH A D25-Jul-20198.3 KiB

Infinite_Set.thyH A D25-Jul-201915.4 KiB

Landau_Symbols.thyH A D25-Jul-2019102.4 KiB

LaTeXsugar.thyH A D25-Jul-20195.5 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-2019813

Library.thyH A D25-Jul-20191.4 KiB

Liminf_Limsup.thyH A D25-Jul-201925.5 KiB

Linear_Temporal_Logic_on_Streams.thyH A D25-Jul-201928.1 KiB

List_Lexorder.thyH A D25-Jul-20193.2 KiB

ListVector.thyH A D25-Jul-20194 KiB

Log_Nat.thyH A D25-Jul-201910.6 KiB

Lub_Glb.thyH A D25-Jul-201910 KiB

Mapping.thyH A D25-Jul-201926.3 KiB

Monad_Syntax.thyH A D25-Jul-20192.2 KiB

More_List.thyH A D25-Jul-201913.3 KiB

Multiset.thyH A D25-Jul-2019141.5 KiB

Multiset_Order.thyH A D25-Jul-201917.1 KiB

Multiset_Permutations.thyH A D25-Jul-201921.7 KiB

multiset_simprocs.MLH A D25-Jul-20191.2 KiB

Nat_Bijection.thyH A D25-Jul-201912.3 KiB

Nonpos_Ints.thyH A D25-Jul-201915.1 KiB

Numeral_Type.thyH A D25-Jul-201916.5 KiB

Old_Datatype.thyH A D25-Jul-201915 KiB

old_recdef.MLH A D25-Jul-2019107.8 KiB

Old_Recdef.thyH A D25-Jul-20192.3 KiB

Omega_Words_Fun.thyH A D25-Jul-201931.4 KiB

Open_State_Syntax.thyH A D25-Jul-20195.4 KiB

Option_ord.thyH A D25-Jul-201918.9 KiB

OptionalSugar.thyH A D25-Jul-20192.3 KiB

Order_Continuity.thyH A D25-Jul-201917.9 KiB

Parallel.thyH A D25-Jul-20191.6 KiB

Pattern_Aliases.thyH A D25-Jul-20197.3 KiB

Periodic_Fun.thyH A D25-Jul-20195.2 KiB

Perm.thyH A D25-Jul-201925.7 KiB

Permutation.thyH A D25-Jul-20199.2 KiB

Permutations.thyH A D25-Jul-201954.4 KiB

Phantom_Type.thyH A D25-Jul-20191.2 KiB

positivstellensatz.MLH A D25-Jul-201934.6 KiB

Predicate_Compile_Alternative_Defs.thyH A D25-Jul-20198.9 KiB

Predicate_Compile_Quickcheck.thyH A D25-Jul-2019352

Prefix_Order.thyH A D25-Jul-20191.9 KiB

Preorder.thyH A D25-Jul-20191.7 KiB

Product_Lexorder.thyH A D25-Jul-20193.3 KiB

Product_Order.thyH A D25-Jul-20199.3 KiB

Product_Plus.thyH A D25-Jul-20193.3 KiB

Quadratic_Discriminant.thyH A D25-Jul-20196.8 KiB

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 D25-Jul-201917.7 KiB

RBT.thyH A D25-Jul-20198.4 KiB

RBT_Impl.thyH A D25-Jul-201995.4 KiB

RBT_Mapping.thyH A D25-Jul-20196.4 KiB

RBT_Set.thyH A D25-Jul-201928.1 KiB

README.htmlH A D25-Jul-20192.6 KiB

Realizers.thyH A D25-Jul-2019349

Reflection.thyH A D25-Jul-20191.1 KiB

refute.MLH A D25-Jul-2019141.8 KiB

Refute.thyH A D25-Jul-20196.4 KiB

rewrite.MLH A D25-Jul-201916.6 KiB

Rewrite.thyH A D25-Jul-20191.2 KiB

Saturated.thyH A D25-Jul-20197.1 KiB

Set_Algebras.thyH A D25-Jul-201913.5 KiB

simps_case_conv.MLH A D25-Jul-20198.2 KiB

Simps_Case_Conv.thyH A D25-Jul-2019263

State_Monad.thyH A D25-Jul-20197.7 KiB

Stirling.thyH A D25-Jul-201910.6 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/H25-Jul-20195

Sum_of_Squares.thyH A D25-Jul-2019535

Transitive_Closure_Table.thyH A D25-Jul-20198 KiB

Tree.thyH A D25-Jul-201916.5 KiB

Tree_Multiset.thyH A D25-Jul-20191.6 KiB

Tree_Real.thyH A D25-Jul-20194.2 KiB

Type_Length.thyH A D25-Jul-20191.7 KiB

Uprod.thyH A D25-Jul-20199 KiB

While_Combinator.thyH A D25-Jul-201917.8 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