Admin/website/faq.html
author haftmann
Sun, 05 Jun 2005 14:33:02 +0200
changeset 16275 951803bff5b1
parent 16241 bf058cdf6841
child 16592 e7df213a1918
permissions -rw-r--r--
a more spohisticated symlink handling
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
     1
<?xml version='1.0' encoding='iso-8859-1' ?>
e634d33deb86 added new website
haftmann
parents:
diff changeset
     2
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
16240
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
     3
<!-- $Id$ -->
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
     4
<html xmlns="http://www.w3.org/1999/xhtml">
e634d33deb86 added new website
haftmann
parents:
diff changeset
     5
e634d33deb86 added new website
haftmann
parents:
diff changeset
     6
<head>
e634d33deb86 added new website
haftmann
parents:
diff changeset
     7
    <title>Isabelle FAQ</title>
e634d33deb86 added new website
haftmann
parents:
diff changeset
     8
    <?include file="//include/htmlheader.include.html"?>
e634d33deb86 added new website
haftmann
parents:
diff changeset
     9
</head>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    10
e634d33deb86 added new website
haftmann
parents:
diff changeset
    11
<body class="main">
e634d33deb86 added new website
haftmann
parents:
diff changeset
    12
    <?include file="//include/header.include.html"?>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    13
    <div class="hr"><hr/></div>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    14
    <?include file="//include/navigation.include.html"?>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    15
    <div class="hr"><hr/></div>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    16
    <div id="content">
e634d33deb86 added new website
haftmann
parents:
diff changeset
    17
e634d33deb86 added new website
haftmann
parents:
diff changeset
    18
    <h2>General Questions</h2>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    19
e634d33deb86 added new website
haftmann
parents:
diff changeset
    20
    <dl class="faq">
e634d33deb86 added new website
haftmann
parents:
diff changeset
    21
e634d33deb86 added new website
haftmann
parents:
diff changeset
    22
      <dt>What is Isabelle?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    23
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    24
      <dd>Isabelle is a popular generic theorem proving environment developed
e634d33deb86 added new website
haftmann
parents:
diff changeset
    25
          at Cambridge University (<a href=
e634d33deb86 added new website
haftmann
parents:
diff changeset
    26
          "http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU Munich
e634d33deb86 added new website
haftmann
parents:
diff changeset
    27
          (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>). See the
e634d33deb86 added new website
haftmann
parents:
diff changeset
    28
          <a href="http://isabelle.in.tum.de/">Isabelle homepage</a> for more
e634d33deb86 added new website
haftmann
parents:
diff changeset
    29
          information.</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    30
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    31
      <dt>Where can I find documentation?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    32
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    33
      <dd><a href="http://isabelle.in.tum.de/docs.html">This way, please</a>.
e634d33deb86 added new website
haftmann
parents:
diff changeset
    34
          Also have a look at the <a href=
e634d33deb86 added new website
haftmann
parents:
diff changeset
    35
          "http://isabelle.in.tum.de/library/">theory library</a>.</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    36
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    37
      <dt>Is it available for download?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    38
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    39
      <dd>Yes, it is available from <a href=
e634d33deb86 added new website
haftmann
parents:
diff changeset
    40
          "http://isabelle.in.tum.de/dist/">several mirror sites</a>. It should run
e634d33deb86 added new website
haftmann
parents:
diff changeset
    41
          on most recent Unix systems (Solaris, Linux, MacOS X, etc.).</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    42
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    43
</dl>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    44
      <h2>Syntax</h2>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    45
e634d33deb86 added new website
haftmann
parents:
diff changeset
    46
    <dl class="faq">
e634d33deb86 added new website
haftmann
parents:
diff changeset
    47
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    48
      <dt>There are lots of arrows in Isabelle. What's the difference between
e634d33deb86 added new website
haftmann
parents:
diff changeset
    49
          <tt>-&gt;</tt>, <tt>=&gt;</tt>, <tt>--&gt;</tt>, and <tt>==&gt;</tt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    50
          ?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    51
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    52
      <dd>Isabelle uses the <tt>=&gt;</tt> arrow for the function type
e634d33deb86 added new website
haftmann
parents:
diff changeset
    53
          (contrary to most functional languages which use <tt>-&gt;</tt>). So
e634d33deb86 added new website
haftmann
parents:
diff changeset
    54
          <tt>a =&gt; b</tt> is the type of a function that takes an element of
e634d33deb86 added new website
haftmann
parents:
diff changeset
    55
          <tt>a</tt> as input and gives you an element of <tt>b</tt> as output. The
e634d33deb86 added new website
haftmann
parents:
diff changeset
    56
          long arrow <tt>--&gt;</tt> and <tt>==&gt;</tt> are object and meta level
e634d33deb86 added new website
haftmann
parents:
diff changeset
    57
          implication. Roughly speaking, the meta level implication should only be
e634d33deb86 added new website
haftmann
parents:
diff changeset
    58
          used when stating theorems where it separates the assumptions from the
e634d33deb86 added new website
haftmann
parents:
diff changeset
    59
          conclusion. Whenever you need an implication inside a HOL formula, use
e634d33deb86 added new website
haftmann
parents:
diff changeset
    60
          <code>--&gt;</code>.</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    61
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    62
      <dt>Where do I have to put those double quotes?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    63
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    64
      <dd>Isabelle distinguishes between <em>inner</em> and <em>outer</em>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    65
          syntax. The outer syntax comes from the Isabelle framework, the inner
e634d33deb86 added new website
haftmann
parents:
diff changeset
    66
          syntax is the one in between quotation marks and comes from the object
e634d33deb86 added new website
haftmann
parents:
diff changeset
    67
          logic (in this case HOL). With time the distinction between the two
e634d33deb86 added new website
haftmann
parents:
diff changeset
    68
          becomes obvious, but in the beginning the following rules of thumb may
e634d33deb86 added new website
haftmann
parents:
diff changeset
    69
          work: types should be inside quotation marks, formulas and lemmas should
e634d33deb86 added new website
haftmann
parents:
diff changeset
    70
          be inside quotation marks, rules and equations (e.g. for definitions)
e634d33deb86 added new website
haftmann
parents:
diff changeset
    71
          should be inside quotation marks, commands like <tt>lemma</tt>,
e634d33deb86 added new website
haftmann
parents:
diff changeset
    72
          <tt>consts</tt>, <tt>primrec</tt>, <tt>constdefs</tt>, <tt>apply</tt>,
e634d33deb86 added new website
haftmann
parents:
diff changeset
    73
          <tt>done</tt> are without quotation marks, as are the names of constants
e634d33deb86 added new website
haftmann
parents:
diff changeset
    74
          in constant definitions (<tt>consts</tt> and <tt>constdefs</tt>)</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    75
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    76
      <dt>What is <tt>"No such constant: _case_syntax"</tt> supposed to tell
e634d33deb86 added new website
haftmann
parents:
diff changeset
    77
          me?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    78
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    79
      <dd>You get this message if you use a case construct on a datatype and
e634d33deb86 added new website
haftmann
parents:
diff changeset
    80
          have a typo in the names of the constructor patterns or if the order of
e634d33deb86 added new website
haftmann
parents:
diff changeset
    81
          the constructors in the case pattern is different from the order in which
e634d33deb86 added new website
haftmann
parents:
diff changeset
    82
          they where defined (in the datatype definition).</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    83
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    84
      <dt>Why doesn't Isabelle understand my equation?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    85
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    86
      <dd>Isabelle's equality <tt>=</tt> binds relatively strongly, so an
e634d33deb86 added new website
haftmann
parents:
diff changeset
    87
          equation like <tt>a = b &amp; c</tt> might not be what you intend.
e634d33deb86 added new website
haftmann
parents:
diff changeset
    88
          Isabelle parses it as <tt>(a = b) &amp; c</tt>. If you want it the other
e634d33deb86 added new website
haftmann
parents:
diff changeset
    89
          way around, you must set explicit parentheses as in <tt>a = (b &amp;
e634d33deb86 added new website
haftmann
parents:
diff changeset
    90
          c)</tt>. This also applies to e.g. <tt>primrec</tt> definitions (see
e634d33deb86 added new website
haftmann
parents:
diff changeset
    91
          below).</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    92
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    93
      <dt>What does it mean "not a proper equation"?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    94
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    95
      <dd>Most commonly this is an instance of the question above. The
e634d33deb86 added new website
haftmann
parents:
diff changeset
    96
          <tt>primrec</tt> command (and others) expect equations as input, and
e634d33deb86 added new website
haftmann
parents:
diff changeset
    97
          since equality binds strongly in Isabelle, something like <tt>f x = b
e634d33deb86 added new website
haftmann
parents:
diff changeset
    98
          &amp; c</tt> is not what you might expect it to be: Isabelle parses it as
e634d33deb86 added new website
haftmann
parents:
diff changeset
    99
          <tt>(f x = b) &amp; c</tt> (which is indeed not a proper equation). To
e634d33deb86 added new website
haftmann
parents:
diff changeset
   100
          turn it into an equation you must set explicit parentheses: <tt>f x = (b
e634d33deb86 added new website
haftmann
parents:
diff changeset
   101
          &amp; c)</tt>.</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   102
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   103
      <dt>What does it mean "<tt>Not a meta-equality (==)</tt>"?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   104
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   105
      <dd>This usually occurs if you use <tt>=</tt> for <tt>constdefs</tt>. The
e634d33deb86 added new website
haftmann
parents:
diff changeset
   106
          <tt>constdefs</tt> and <tt>defs</tt> commands expect not equations, but
e634d33deb86 added new website
haftmann
parents:
diff changeset
   107
          meta equivalences. Just use the <tt>\&lt;equiv&gt;</tt> or <tt>==</tt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   108
          signs instead of <tt>=</tt>.</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   109
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   110
</dl>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   111
      <h2>Proving</h2>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   112
e634d33deb86 added new website
haftmann
parents:
diff changeset
   113
    <dl class="faq">
e634d33deb86 added new website
haftmann
parents:
diff changeset
   114
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   115
      <dt>What does "empty result sequence" mean?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   116
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   117
      <dd>It means that the applied proof method (or tactic) was unsuccessful.
e634d33deb86 added new website
haftmann
parents:
diff changeset
   118
          It did not transform the goal in any way, or simply just failed to do
e634d33deb86 added new website
haftmann
parents:
diff changeset
   119
          anything. You must try another tactic (or give the one you used more
e634d33deb86 added new website
haftmann
parents:
diff changeset
   120
          hints or lemmas to work with)</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   121
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   122
      <dt>The Simplifier doesn't want to apply my rule, what's wrong?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   123
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   124
      <dd>Most commonly this is a typing problem. The rule you want to apply
e634d33deb86 added new website
haftmann
parents:
diff changeset
   125
          may require a more special (or just plain different) type from what you
e634d33deb86 added new website
haftmann
parents:
diff changeset
   126
          have in the current goal. Use the ProofGeneral menu <tt>Isabelle/Isar
e634d33deb86 added new website
haftmann
parents:
diff changeset
   127
          -&gt; Settings -&gt; Show Types</tt> and the <tt>thm</tt> command on the
e634d33deb86 added new website
haftmann
parents:
diff changeset
   128
          rule you want to apply to find out if the types are what you expect them
e634d33deb86 added new website
haftmann
parents:
diff changeset
   129
          to be (also take a look at the types in your goal). <tt>Show Sorts</tt>,
e634d33deb86 added new website
haftmann
parents:
diff changeset
   130
          <tt>Show Constants</tt>, and <tt>Trace Simplifier</tt> in the same menu
e634d33deb86 added new website
haftmann
parents:
diff changeset
   131
          may also be helpful.</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   132
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   133
      <dt>If I do <tt>auto</tt>, it leaves me a goal <tt>False</tt>. Is my
e634d33deb86 added new website
haftmann
parents:
diff changeset
   134
          theorem wrong?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   135
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   136
      <dd>Not necessarily. It just means that <tt>auto</tt> transformed the
e634d33deb86 added new website
haftmann
parents:
diff changeset
   137
          goal into something that is not provable any more. That could be due to
e634d33deb86 added new website
haftmann
parents:
diff changeset
   138
          <tt>auto</tt> doing something stupid, or e.g. due to some earlier step in
e634d33deb86 added new website
haftmann
parents:
diff changeset
   139
          the proof that lost important information. It is of course also possible
e634d33deb86 added new website
haftmann
parents:
diff changeset
   140
          that the goal was never provable in the first place.</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   141
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   142
      <dt>Why does <tt>lemma "1+1=2"</tt> fail?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   143
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   144
      <dd>Because it is not necessarily true. Isabelle does not assume that 1
e634d33deb86 added new website
haftmann
parents:
diff changeset
   145
          and 2 are natural numbers. Try <tt>"(1::nat)+1=2"</tt> instead.</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   146
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   147
      <dt>Can Isabelle find counterexamples?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   148
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   149
      <dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   150
            <p>For arithmetic goals, <code>arith</code> finds counterexamples. For
e634d33deb86 added new website
haftmann
parents:
diff changeset
   151
            executable goals, <code>quickcheck</code> tries to find a
e634d33deb86 added new website
haftmann
parents:
diff changeset
   152
            counterexample. For goals of a more logical nature (including
e634d33deb86 added new website
haftmann
parents:
diff changeset
   153
            quantifiers, sets and inductive definitions) <code>refute</code>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   154
            searches for a countermodel.</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   155
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   156
            <p>Otherwise, negate the proposition and instantiate (some) variables
e634d33deb86 added new website
haftmann
parents:
diff changeset
   157
            with concrete values. You may also need additional assumptions about
e634d33deb86 added new website
haftmann
parents:
diff changeset
   158
            these values. For example, <tt>True &amp; False ~= True | False</tt> is
e634d33deb86 added new website
haftmann
parents:
diff changeset
   159
            a counterexample of <tt>A &amp; B = A | B</tt>, and <tt>A = ~B ==&gt; A
e634d33deb86 added new website
haftmann
parents:
diff changeset
   160
            &amp; B ~= A | B</tt> is another one. Sometimes Isabelle can help you
e634d33deb86 added new website
haftmann
parents:
diff changeset
   161
            to find the counterexample: just negate the proposition and do
e634d33deb86 added new website
haftmann
parents:
diff changeset
   162
            <tt>auto</tt> or <tt>simp</tt>. If lucky, you are left with the
e634d33deb86 added new website
haftmann
parents:
diff changeset
   163
            assumptions you need for the counterexample to work.</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   164
          </dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   165
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   166
</dl>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   167
      <h2>Interface</h2>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   168
e634d33deb86 added new website
haftmann
parents:
diff changeset
   169
    <dl class="faq">
e634d33deb86 added new website
haftmann
parents:
diff changeset
   170
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   171
      <dt>ProofGeneral appears to hang when Isabelle is started.</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   172
      <dd><p>This may be because of UTF-8 issues e.g. in Red Hat 8.0/9.0, Suse
e634d33deb86 added new website
haftmann
parents:
diff changeset
   173
      9.0/9.1</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   174
      <p>RedHat 8 and later has glibc 2.2 and UTF8 encoded output may be turned on
e634d33deb86 added new website
haftmann
parents:
diff changeset
   175
      in default locale. Unfortunately Proof General relies on 8-bit characters
e634d33deb86 added new website
haftmann
parents:
diff changeset
   176
      which are UTF8 prefixes in the output of proof assistants (inc Coq,
e634d33deb86 added new website
haftmann
parents:
diff changeset
   177
      Isabelle). These prefix characters are not flushed to stdout individually. As
e634d33deb86 added new website
haftmann
parents:
diff changeset
   178
      a workaround we must find a way to disable interpretation of UTF8 in the C
e634d33deb86 added new website
haftmann
parents:
diff changeset
   179
      libraries that Coq and friends use.</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   180
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   181
      <p>Doing this inside PG/Emacs seems tricky; locale settings are set/inherited
e634d33deb86 added new website
haftmann
parents:
diff changeset
   182
      in strange ways. One solution is to run the Emacs process itself with an
e634d33deb86 added new website
haftmann
parents:
diff changeset
   183
      altered locale setting, for example, starting XEmacs by typing:</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   184
    
16240
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   185
      <ul class="shellcmd">
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   186
        <li>LC_CTYPE=en_GB Isabelle &amp;</li>
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   187
      </ul>
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
   188
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   189
      <p>The supplied proofgeneral script makes this setting if it sees the string
16240
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   190
      UTF in the current value of <tt class="shellcmd">LC_CTYPE</tt>.
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   191
      Depending on your distribution, this
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   192
      variable might also be called <tt class="shellcmd">LANG</tt>.</p>
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
   193
    
16240
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   194
      <p>Alternatively you can set <tt class="shellcmd">LC_CTYPE</tt> or
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   195
      <tt class="shellcmd">LANG</tt> inside a file <tt class="shellcmd">~/.i18n</tt>, which
16241
bf058cdf6841 adjusted navigation width
haftmann
parents: 16240
diff changeset
   196
      will be read by the shell. This will affect all applications, though.</p>
16240
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   197
      
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   198
      <p>Suggestions for a better workaround inside Emacs would be welcomed;</p>
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
   199
    
16240
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   200
      <p>A related issue is warnings from x-symbol: "Emacs language environment
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
   201
      and system locale specify different encoding, I'll assume `iso-8859-1'". This
e634d33deb86 added new website
haftmann
parents:
diff changeset
   202
      warning appears to be mainly harmless. Notice that the variable
e634d33deb86 added new website
haftmann
parents:
diff changeset
   203
      `buffer-file-coding-system' may determine the format that files are saved
e634d33deb86 added new website
haftmann
parents:
diff changeset
   204
      in.</p></dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   205
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   206
      <dt>X-Symbol doesn't seem to work. What can I do?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   207
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   208
      <dd>The most common reason why X-Symbol doesn't work is: it's not
e634d33deb86 added new website
haftmann
parents:
diff changeset
   209
          switched on yet. Assuming you are using ProofGeneral and have installed
e634d33deb86 added new website
haftmann
parents:
diff changeset
   210
          the X-Symbol package, you still need to turn X-Symbol on in ProofGeneral:
e634d33deb86 added new website
haftmann
parents:
diff changeset
   211
          select the menu items <tt>Proof-General -&gt; Options -&gt; X-Symbol</tt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   212
          and (if you want to save the setting for future sessions) select
e634d33deb86 added new website
haftmann
parents:
diff changeset
   213
          <tt>Options -&gt; Save Options</tt> in XEmacs.</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   214
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   215
      <dt>How do I input those X-Symbols anyway?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   216
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   217
      <dd>There are lots of ways to input x-symbols. The one that always works
e634d33deb86 added new website
haftmann
parents:
diff changeset
   218
          is writing it out in plain text (e.g. for the 'and' symbol type
e634d33deb86 added new website
haftmann
parents:
diff changeset
   219
          <tt>\&lt;and&gt;</tt>). For common symbols you can try to "paint them in
e634d33deb86 added new website
haftmann
parents:
diff changeset
   220
          ASCII" and if the xsymbol package recognizes them it will automatically
e634d33deb86 added new website
haftmann
parents:
diff changeset
   221
          convert them into their graphical representation. Examples:
e634d33deb86 added new website
haftmann
parents:
diff changeset
   222
          <tt>--&gt;</tt> is converted into the long single arrow, <tt>/\</tt> is
e634d33deb86 added new website
haftmann
parents:
diff changeset
   223
          converted into the 'and' symbol, the sequence <tt>=_</tt> into the
e634d33deb86 added new website
haftmann
parents:
diff changeset
   224
          equivalence sign, <tt>&lt;_</tt> into less-or-equal, <tt>[|</tt> into
e634d33deb86 added new website
haftmann
parents:
diff changeset
   225
          opening semantic brackets, and so on. For greek characters, the
e634d33deb86 added new website
haftmann
parents:
diff changeset
   226
          <code>rotate</code> command works well: to input &alpha; type
e634d33deb86 added new website
haftmann
parents:
diff changeset
   227
          <code>a</code> and then <code>C-.</code> (control and <code>.</code>).
e634d33deb86 added new website
haftmann
parents:
diff changeset
   228
          You can also display the grid-of-characters in the x-symbol menu to get
e634d33deb86 added new website
haftmann
parents:
diff changeset
   229
          an overview of the available graphical representations (not all of them
e634d33deb86 added new website
haftmann
parents:
diff changeset
   230
          already have a meaning in Isabelle, though).</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   231
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   232
</dl>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   233
      <h2>System</h2>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   234
e634d33deb86 added new website
haftmann
parents:
diff changeset
   235
    <dl class="faq">
e634d33deb86 added new website
haftmann
parents:
diff changeset
   236
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   237
      <dt>I want to generate one of those flashy LaTeX documents. How?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   238
    
16240
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   239
      <dd>You will need to work with the <tt class="shellcmd">isatool</tt> command for this (in
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
   240
          a Unix shell). The easiest way to get to a document is the following: use
16240
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   241
          <tt class="shellcmd">isatool mkdir</tt> to set up a new directory. The command will also
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   242
          create a file called <tt class="shellcmd">IsaMakefile</tt> in the current directory. Put
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
   243
          your theory file(s) into the new directory and edit the file
16240
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   244
          <tt class="shellcmd">ROOT.ML</tt> in there (following the comments) to tell Isabelle which
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
   245
          of the theories to load (and in which order). Go back to the parent
16240
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   246
          directory (where the <tt class="shellcmd">IsaMakefile</tt> is) and type <tt class="shellcmd">isatool
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
   247
          make</tt>. Isabelle should then process your theories and tell you where
e634d33deb86 added new website
haftmann
parents:
diff changeset
   248
          to find the finished document. For more information on generating
e634d33deb86 added new website
haftmann
parents:
diff changeset
   249
          documents see the Isabelle Tutorial, Chapter 4.</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   250
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   251
      <dt>I have a large formalization with many theories. Must I process all
e634d33deb86 added new website
haftmann
parents:
diff changeset
   252
          of them all of the time?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   253
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   254
      <dd>No, you can tell Isabelle to build a so-called heap image. This heap
e634d33deb86 added new website
haftmann
parents:
diff changeset
   255
          image can contain your preloaded theories. To get one, set up a directory
16240
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   256
          with a <tt class="shellcmd">ROOT.ML</tt> file (as for generating a document) and use the
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   257
          command <tt class="shellcmd">isatool usedir -b HOL MyImage</tt> in that directory to
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   258
          create an image <tt class="shellcmd">MyImage</tt> using the parent logic <tt class="shellcmd">HOL</tt>. You
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   259
          should then be able to invoke Isabelle with <tt class="shellcmd">Isabelle -l MyImage</tt>
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
   260
          and have everything that is loaded in ROOT.ML instantly available.</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   261
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   262
      <dt>Does Isabelle run on Windows?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   263
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   264
      <dd>After a fashion, yes, but Isabelle is not being developed for
e634d33deb86 added new website
haftmann
parents:
diff changeset
   265
          Windows. See the <a href="dist/installation_notes_cygwin.html">installation notes</a> for windows.
e634d33deb86 added new website
haftmann
parents:
diff changeset
   266
          If the approach presented there is not sufficient for your purpose, consider a
e634d33deb86 added new website
haftmann
parents:
diff changeset
   267
          dualboot Windows/Linux system.</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   268
e634d33deb86 added new website
haftmann
parents:
diff changeset
   269
    </dl>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   270
e634d33deb86 added new website
haftmann
parents:
diff changeset
   271
    </div>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   272
    <div class="hr"><hr/></div>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   273
    <?include file="//include/footer.include.html"?>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   274
</body>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   275
e634d33deb86 added new website
haftmann
parents:
diff changeset
   276
</html>