# HG changeset patch
# User kleing
# Date 1082100452 -7200
# Node ID f0779f6fa7e881773867532f56ddf3917a4a42c2
# Parent  f56e9e16753b30319a46b3d9d5a4ccd4d13f8973
make weblint happy

diff -r f56e9e16753b -r f0779f6fa7e8 Admin/page/Makefile
--- a/Admin/page/Makefile	Fri Apr 16 09:01:55 2004 +0200
+++ b/Admin/page/Makefile	Fri Apr 16 09:27:32 2004 +0200
@@ -55,8 +55,8 @@
 	@cp -R main/. ../../main-`cat DISTNAME`/.
 
 weblint:
-	-weblint -x netscape $(MAIN_TARGET)
-	-weblint -x netscape $(DIST_TARGET)
+	-weblint -x netscape -d extension-attribute -e img-size $(MAIN_TARGET)
+	-weblint -x netscape -d extension-attribute -e img-size $(DIST_TARGET)
 
 clean: 
 	@rm -rf $(MAIN_TARGET)
diff -r f56e9e16753b -r f0779f6fa7e8 Admin/page/main-content/faq.content
--- a/Admin/page/main-content/faq.content	Fri Apr 16 09:01:55 2004 +0200
+++ b/Admin/page/main-content/faq.content	Fri Apr 16 09:27:32 2004 +0200
@@ -57,21 +57,21 @@
     <table class="question" width="100%">
         <tr>
           <td>There are lots of arrows in Isabelle. What's the
-          difference between <tt>-></tt>, <tt>=></tt>, <tt>--></tt>,
-          and <tt>==></tt> ?</td>
+          difference between <tt>-&gt;</tt>, <tt>=&gt;</tt>, <tt>--&gt;</tt>,
+          and <tt>==&gt;</tt> ?</td>
         </tr>
     </table>
     <table class="answer" width="100%">
-        <tr><td>Isabelle uses the <tt>=></tt> arrow for the function
+        <tr><td>Isabelle uses the <tt>=&gt;</tt> arrow for the function
         type (contrary to most functional languages which use
-        <tt>-></tt>). So <tt>a => b</tt> is the type of a function
+        <tt>-&gt;</tt>). So <tt>a =&gt; b</tt> is the type of a function
         that takes an element of <tt>a</tt> as input and gives you an
-        element of <tt>b</tt> as output. The long arrow <tt>--></tt>
-        and <tt>==></tt> are object and meta level
+        element of <tt>b</tt> as output. The long arrow <tt>--&gt;</tt>
+        and <tt>==&gt;</tt> are object and meta level
         implication. Roughly speaking, the meta level implication
         should only be used when stating theorems where it separates
         the assumptions from the conclusion. Whenever you need an
-        implication inside a HOL formula, use <code>--></code>.
+        implication inside a HOL formula, use <code>--&gt;</code>.
         </td></tr>
     </table>
 
@@ -153,7 +153,7 @@
     Most commonly this is a typing problem. The rule you want to apply
     may require a more special (or just plain different) type from
     what you have in the current goal. Use the ProofGeneral menu
-    <tt>Isabelle/Isar -> Settings -> Show Types</tt> and the
+    <tt>Isabelle/Isar -&gt; Settings -&gt; Show Types</tt> and the
     <tt>thm</tt> command on the rule you want to apply to find out if
     the types are what you expect them to be (also take a look at the
     types in your goal). <tt>Show Sorts</tt>, <tt>Show Constants</tt>,
@@ -198,7 +198,7 @@
     and instantiate (some) variables with concrete values. You may
     also need additional assumptions about these values.  For example,
     <tt>True & False ~= True | False</tt> is a counterexample of <tt>A
-    & B = A | B</tt>, and <tt>A = ~B ==> A & B ~= A | B</tt> is
+    & B = A | B</tt>, and <tt>A = ~B ==&gt; A & B ~= A | B</tt> is
     another one. Sometimes Isabelle can help you to find the
     counterexample: just negate the proposition and do <tt>auto</tt>
     or <tt>simp</tt>.  If lucky, you are left with the assumptions you
@@ -216,8 +216,8 @@
     work is: it's not switched on yet. Assuming you are using
     ProofGeneral and have installed the X-Symbol package, you still
     need to turn X-Symbol on in ProofGeneral: select the menu items
-    <tt>Proof-General -> Options -> X-Symbol</tt> and (if you want to
-    save the setting for future sessions) select <tt>Options -> Save
+    <tt>Proof-General -&gt; Options -&gt; X-Symbol</tt> and (if you want to
+    save the setting for future sessions) select <tt>Options -&gt; Save
     Options</tt> in XEmacs.</td></tr></table>
 
     <table class="question" width="100%"><tr><td>How do I input those X-Symbols anyway?</td></tr></table>
@@ -228,9 +228,9 @@
     type <tt>\&lt;and&gt;</tt>). For common symbols you can try to "paint
     them in ASCII" and if the xsymbol package recognizes them it will
     automatically convert them into their graphical
-    representation. Examples: <tt>--></tt> is converted into the long
+    representation. Examples: <tt>--&gt;</tt> is converted into the long
     single arrow, <tt>/\</tt> is converted into the 'and' symbol, the
-    sequence <tt>=_</tt> into the equivalence sign, <tt><_</tt> into
+    sequence <tt>=_</tt> into the equivalence sign, <tt>&lt;_</tt> into
     less-or-equal, <tt>[|</tt> into opening semantic brackets, and so
     on. For greek characters, the <code>rotate</code> command works well:
     to input &alpha; type <code>a</code> and then <code>C-.</code>
diff -r f56e9e16753b -r f0779f6fa7e8 Admin/page/main-content/index.content
--- a/Admin/page/main-content/index.content	Fri Apr 16 09:01:55 2004 +0200
+++ b/Admin/page/main-content/index.content	Fri Apr 16 09:27:32 2004 +0200
@@ -46,11 +46,7 @@
 <li>Type <code>rat</code> of the rational numbers available in HOL-Complex.</li>
 
 <li>Improved locales (named proof contexts), instantiation of locales.</li>
-<!--
-<li>Improved calculational reasoning chains.</li>
 
-<li>Improved records handling.</li>
-//-->
 <li>Improved handling of linear and partial orders in simplifier.</li>
  
 <li>New <code>specification</code> command for definition by specification.</li>