--- a/src/HOL/Library/README.html Fri Jun 27 11:30:42 2014 +0200
+++ b/src/HOL/Library/README.html Fri Jun 27 15:24:56 2014 +0200
@@ -23,12 +23,6 @@
<dl>
-<dt><strong>Files</strong>
-
-<dd>Avoid unnecessary scattering of theories over several files. Use
-new-style theories only, as old ones tend to clutter the file space
-with separate <tt>.thy</tt> and <tt>.ML</tt> files.
-
<dt><strong>Examples</strong>
<dd>Theories should be as ``generic'' as is sensible. Unused (or
@@ -54,12 +48,6 @@
separate word constituents by underscores, as in <tt>foo_bar</tt> or
<tt>Foo_Bar</tt> (this looks best in LaTeX output).
-<p>
-
-Note that syntax is <em>global</em>; qualified names lose syntax on
-output. Do not use ``exotic'' symbols for syntax (such as
-<tt>\<oplus></tt>), but leave these for user applications.
-
<dt><strong>Global context declarations</strong>
<dd>Only items introduced in the present theory should be declared
@@ -67,42 +55,6 @@
rules from parent theories may result in strange behavior later,
depending on the user's arrangement of import lists.
-<dt><strong>Mathematical symbols</strong>
-
-<dd>Non-ASCII symbols should be used as appropriate, with some
-care. In particular, avoid unreadable arrows: <tt>==></tt> should
-be preferred over <tt>\<Longrightarrow></tt>. Use <tt>isabelle
-unsymbolize</tt> to clean up the sources.
-
-<p>
-
-The following ASCII symbols of HOL should be generally avoided:
-<tt>@</tt>, <tt>!</tt>, <tt>?</tt>, <tt>?!</tt>, <tt>%</tt>, better
-use <tt>SOME</tt>, <tt>ALL</tt> (or <tt>\<forall></tt>),
-<tt>EX</tt> (or <tt>\<exists></tt>), <tt>EX!</tt> (or
-<tt>\<exists>!</tt>), <tt>\<lambda></tt>, respectively.
-Note that bracket notation <tt>[| |]</tt> looks bad in LaTeX
-output.
-
-<p>
-
-Some additional mathematical symbols are quite suitable for both
-readable sources and the output document:
-<tt>\<Inter></tt>,
-<tt>\<Union></tt>,
-<tt>\<and></tt>,
-<tt>\<in></tt>,
-<tt>\<inter></tt>,
-<tt>\<le></tt>,
-<tt>\<not></tt>,
-<tt>\<noteq></tt>,
-<tt>\<notin></tt>,
-<tt>\<or></tt>,
-<tt>\<subset></tt>,
-<tt>\<subseteq></tt>,
-<tt>\<times></tt>,
-<tt>\<union></tt>.
-
<dt><strong>Spacing</strong>
<dd>Isabelle is able to produce a high-quality LaTeX document from the
@@ -111,10 +63,8 @@
text. Incidentally, output looks very good if common type-setting
conventions are observed: put a single space <em>after</em> each
punctuation character ("<tt>,</tt>", "<tt>.</tt>", etc.), but none
-before it; do not extra spaces inside of parentheses, unless the
-delimiters are composed of multiple symbols (as in
-<tt>[| |]</tt>); do not attempt to simulate table markup with
-spaces, avoid ``hanging'' indentations.
+before it; do not extra spaces inside of parentheses; do not attempt
+to simulate table markup with spaces, avoid ``hanging'' indentations.
</dl>