author | wenzelm |
Fri, 19 Aug 2022 23:58:44 +0200 | |
changeset 75916 | b6589c8ccadd |
permissions | -rw-r--r-- |
75916
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
1 |
theory README imports Main |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
2 |
begin |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
3 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
4 |
section \<open>HOL-Library: supplemental theories for main Isabelle/HOL\<close> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
5 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
6 |
text \<open> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
7 |
This is a collection of generic theories that may be used together with main |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
8 |
Isabelle/HOL. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
9 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
10 |
Addition of new theories should be done with some care, as the ``module |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
11 |
system'' of Isabelle is rather simplistic. The following guidelines may be |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
12 |
helpful to achieve maximum re-usability and minimum clashes with existing |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
13 |
developments. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
14 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
15 |
\<^descr>[Examples] Theories should be as ``generic'' as is sensible. Unused (or |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
16 |
rather unusable?) theories should be avoided; common applications should |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
17 |
actually refer to the present theory. Small example uses may be included in |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
18 |
the library as well, but should be put in a separate theory, such as |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
19 |
\<^verbatim>\<open>Foobar.thy\<close> accompanied by \<^verbatim>\<open>Foobar_Examples.thy\<close>. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
20 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
21 |
\<^descr>[Names of logical items] There are separate hierarchically structured name |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
22 |
spaces for types, constants, theorems etc. Nevertheless, some care should be |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
23 |
taken, as the name spaces are always ``open''. Use adequate names; avoid |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
24 |
unreadable abbreviations. The general naming convention is to separate word |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
25 |
constituents by underscores, as in \<^verbatim>\<open>foo_bar\<close> or \<^verbatim>\<open>Foo_Bar\<close> (this looks best |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
26 |
in LaTeX output). |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
27 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
28 |
\<^descr>[Global context declarations] Only items introduced in the present theory |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
29 |
should be declared globally (e.g. as Simplifier rules). Note that adding and |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
30 |
deleting rules from parent theories may result in strange behavior later, |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
31 |
depending on the user's arrangement of import lists. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
32 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
33 |
\<^descr>[Spacing] Isabelle is able to produce a high-quality LaTeX document from |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
34 |
the theory sources, provided some minor issues are taken care of. In |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
35 |
particular, spacing and line breaks are directly taken from source text. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
36 |
Incidentally, output looks very good if common type-setting conventions are |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
37 |
observed: put a single space \<^emph>\<open>after\<close> each punctuation character ("\<^verbatim>\<open>,\<close>", |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
38 |
"\<^verbatim>\<open>.\<close>", etc.), but none before it; do not extra spaces inside of |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
39 |
parentheses; do not attempt to simulate table markup with spaces, avoid |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
40 |
``hanging'' indentations. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
41 |
\<close> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
42 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
43 |
end |