Admin/website/faq.html

           "http://isabelle.in.tum.de/dist/library/">theory library</a>.</dd>
     
       <dt>Is it available for download?</dt>
     
       <dd>Yes, it is available from several mirror sites, e.&nbsp;g. from
-          <a href="http://isabelle.in.tum.de">Munich</a>. It should run
-          on most recent Unix systems (Solaris, Linux, MacOS&nbsp;X, etc.).</dd>
+          <a href="http://isabelle.in.tum.de">Munich</a>. It runs on common
+          Unix systems (Linux, MacOS&nbsp;X, Solaris, etc.).</dd>
     
 </dl>
       <h2>Syntax</h2>
 
     <dl class="faq">
     
-      <dt>There are lots of arrows in Isabelle. What's the difference between
+      <dt>There are lots of arrows in Isabelle/HOL. What's the difference between
           <tt>-&gt;</tt>, <tt>=&gt;</tt>, <tt>--&gt;</tt>, and <tt>==&gt;</tt>
           ?</dt>
     
       <dd>Isabelle uses the <tt>=&gt;</tt> arrow for the function type
           (contrary to most functional languages which use <tt>-&gt;</tt>). So

       <dd>You get this message if you use a case construct on a datatype and
           have a typo in the names of the constructor patterns or if the order of
           the constructors in the case pattern is different from the order in which
           they where defined (in the datatype definition).</dd>
     
-      <dt>Why doesn't Isabelle understand my equation?</dt>
+      <dt>Why doesn't Isabelle/HOL understand my equation?</dt>
     
       <dd>Isabelle's equality <tt>=</tt> binds relatively strongly, so an
           equation like <tt>a = b &amp; c</tt> might not be what you intend.
           Isabelle parses it as <tt>(a = b) &amp; c</tt>. If you want it the other
           way around, you must set explicit parentheses as in <tt>a = (b &amp;

     
       <dt>What does it mean "not a proper equation"?</dt>
     
       <dd>Most commonly this is an instance of the question above. The
           <tt>primrec</tt> command (and others) expect equations as input, and
-          since equality binds strongly in Isabelle, something like <tt>f x = b
+          since equality binds strongly in Isabelle/HOL, something like <tt>f x = b
           &amp; c</tt> is not what you might expect it to be: Isabelle parses it as
           <tt>(f x = b) &amp; c</tt> (which is indeed not a proper equation). To
           turn it into an equation you must set explicit parentheses: <tt>f x = (b
           &amp; c)</tt>.</dd>
     

           the proof that lost important information. It is of course also possible
           that the goal was never provable in the first place.</dd>
     
       <dt>Why does <tt>lemma "1+1=2"</tt> fail?</dt>
     
-      <dd>Because it is not necessarily true. Isabelle does not assume that 1
+      <dd>Because it is not necessarily true. Isabelle/HOL does not assume that 1
           and 2 are natural numbers. Try <tt>"(1::nat)+1=2"</tt> instead.</dd>
     
-      <dt>Can Isabelle find counterexamples?</dt>
+      <dt>Can Isabelle/HOL find counterexamples?</dt>
     
       <dd>
             <p>For arithmetic goals, <code>arith</code> finds counterexamples. For
             executable goals, <code>quickcheck</code> tries to find a
             counterexample. For goals of a more logical nature (including

 </dl>
       <h2>Interface</h2>
 
     <dl class="faq">
     
-      <dt>ProofGeneral appears to hang when Isabelle is started.</dt>
-      <dd><p>This may be because of UTF-8 issues e.g. in Red Hat 8.0/9.0, Suse
-      9.0/9.1</p>
-      <p>RedHat 8 and later has glibc 2.2 and UTF8 encoded output may be turned on
-      in default locale. Unfortunately Proof General relies on 8-bit characters
-      which are UTF8 prefixes in the output of proof assistants (inc Coq,
-      Isabelle). These prefix characters are not flushed to stdout individually. As
-      a workaround we must find a way to disable interpretation of UTF8 in the C
-      libraries that Coq and friends use.</p>
-    
-      <p>Doing this inside PG/Emacs seems tricky; locale settings are set/inherited
-      in strange ways. One solution is to run the Emacs process itself with an
-      altered locale setting, for example, starting XEmacs by typing:</p>
-    
-      <ul class="shellcmd">
-        <li>LC_CTYPE=en_GB Isabelle &amp;</li>
-      </ul>
-    
-      <p>The supplied proofgeneral script makes this setting if it sees the string
-      UTF in the current value of <tt class="shellcmd">LC_CTYPE</tt>.
-      Depending on your distribution, this
-      variable might also be called <tt class="shellcmd">LANG</tt>.</p>
-    
-      <p>Alternatively you can set <tt class="shellcmd">LC_CTYPE</tt> or
-      <tt class="shellcmd">LANG</tt> inside a file <tt class="shellcmd">~/.i18n</tt>, which
-      will be read by the shell. This will affect all applications, though.</p>
-      
-      <p>Suggestions for a better workaround inside Emacs would be welcomed;</p>
-    
-      <p>A related issue is warnings from x-symbol: "Emacs language environment
-      and system locale specify different encoding, I'll assume `iso-8859-1'". This
-      warning appears to be mainly harmless. Notice that the variable
-      `buffer-file-coding-system' may determine the format that files are saved
-      in.</p></dd>
-    
       <dt>X-Symbol doesn't seem to work. What can I do?</dt>
     
       <dd>The most common reason why X-Symbol doesn't 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 -&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.</dd>
-    
+
       <dt>How do I input those X-Symbols anyway?</dt>
     
       <dd>There are lots of ways to input x-symbols. The one that always works
           is writing it out in plain text (e.g. for the 'and' symbol type
           <tt>\&lt;and&gt;</tt>). For common symbols you can try to "paint them in

           with a <tt class="shellcmd">ROOT.ML</tt> file (as for generating a document) and use the
           command <tt class="shellcmd">isatool usedir -b HOL MyImage</tt> in that directory to
           create an image <tt class="shellcmd">MyImage</tt> using the parent logic <tt class="shellcmd">HOL</tt>. You
           should then be able to invoke Isabelle with <tt class="shellcmd">Isabelle -l MyImage</tt>
           and have everything that is loaded in ROOT.ML instantly available.</dd>
+
+      <dt>Can I run Isabelle on Windows?</dt>
+
+      <dd>Not really.  The Cygwin environment provides a Unixoid
+      look-and-feel that is sufficient for very basic Isabelle
+      functionality.  See also <a
+      href="installation_notes_cygwin.html">Installation notes for
+      Cygwin/Windows.</a>
+
+      To try out Isabelle it might be much easier to use a Linux boot
+      CD, such as <a href="http://www.knoppix.org/">Knoppix</a>.</dd>
     
     </dl>
 
     </div>
     <div class="hr"><hr/></div>