changeset 57412 b441f330078b
parent 42062 9fe5daa2e705
--- 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 @@
-<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.
 <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).
-Note that syntax is <em>global</em>; qualified names lose syntax on
-output.  Do not use ``exotic'' symbols for syntax (such as
-<tt>\&lt;oplus&gt;</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>==&gt;</tt> should
-be preferred over <tt>\&lt;Longrightarrow&gt;</tt>. Use <tt>isabelle
-unsymbolize</tt> to clean up the sources.
-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>\&lt;forall&gt;</tt>),
-<tt>EX</tt> (or <tt>\&lt;exists&gt;</tt>), <tt>EX!</tt> (or
-<tt>\&lt;exists&gt;!</tt>), <tt>\&lt;lambda&gt;</tt>, respectively.
-Note that bracket notation <tt>[|&nbsp;|]</tt> looks bad in LaTeX
-Some additional mathematical symbols are quite suitable for both
-readable sources and the output document:
 <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>[|&nbsp;|]</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.