Admin/website/faq.html
author wenzelm
Wed, 15 Feb 2006 21:34:55 +0100
changeset 19046 bc5c6c9b114e
parent 17661 994d010c0abd
permissions -rw-r--r--
removed distinct, renamed gen_distinct to distinct;
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
    
17563
abb280dd3431 unify dist and main
haftmann
parents: 16592
diff changeset
    33
      <dd><a href="http://isabelle.in.tum.de/documentation.html">This way, please</a>.
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
    34
          Also have a look at the <a href=
17563
abb280dd3431 unify dist and main
haftmann
parents: 16592
diff changeset
    35
          "http://isabelle.in.tum.de/dist/library/">theory library</a>.</dd>
16233
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
    
17563
abb280dd3431 unify dist and main
haftmann
parents: 16592
diff changeset
    39
      <dd>Yes, it is available from several mirror sites, e.&nbsp;g. from
17661
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
    40
          <a href="http://isabelle.in.tum.de">Munich</a>. It runs on common
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
    41
          Unix systems (Linux, MacOS&nbsp;X, Solaris, etc.).</dd>
16233
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
    
17661
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
    48
      <dt>There are lots of arrows in Isabelle/HOL. What's the difference between
16233
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
    
17661
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
    84
      <dt>Why doesn't Isabelle/HOL understand my equation?</dt>
16233
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
17661
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
    97
          since equality binds strongly in Isabelle/HOL, something like <tt>f x = b
16233
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
    
17661
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
   144
      <dd>Because it is not necessarily true. Isabelle/HOL does not assume that 1
16233
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
    
17661
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
   147
      <dt>Can Isabelle/HOL find counterexamples?</dt>
16233
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>X-Symbol doesn't seem to work. What can I do?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   172
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   173
      <dd>The most common reason why X-Symbol doesn't work is: it's not
e634d33deb86 added new website
haftmann
parents:
diff changeset
   174
          switched on yet. Assuming you are using ProofGeneral and have installed
e634d33deb86 added new website
haftmann
parents:
diff changeset
   175
          the X-Symbol package, you still need to turn X-Symbol on in ProofGeneral:
e634d33deb86 added new website
haftmann
parents:
diff changeset
   176
          select the menu items <tt>Proof-General -&gt; Options -&gt; X-Symbol</tt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   177
          and (if you want to save the setting for future sessions) select
e634d33deb86 added new website
haftmann
parents:
diff changeset
   178
          <tt>Options -&gt; Save Options</tt> in XEmacs.</dd>
17661
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
   179
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
   180
      <dt>How do I input those X-Symbols anyway?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   181
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   182
      <dd>There are lots of ways to input x-symbols. The one that always works
e634d33deb86 added new website
haftmann
parents:
diff changeset
   183
          is writing it out in plain text (e.g. for the 'and' symbol type
e634d33deb86 added new website
haftmann
parents:
diff changeset
   184
          <tt>\&lt;and&gt;</tt>). For common symbols you can try to "paint them in
e634d33deb86 added new website
haftmann
parents:
diff changeset
   185
          ASCII" and if the xsymbol package recognizes them it will automatically
e634d33deb86 added new website
haftmann
parents:
diff changeset
   186
          convert them into their graphical representation. Examples:
e634d33deb86 added new website
haftmann
parents:
diff changeset
   187
          <tt>--&gt;</tt> is converted into the long single arrow, <tt>/\</tt> is
e634d33deb86 added new website
haftmann
parents:
diff changeset
   188
          converted into the 'and' symbol, the sequence <tt>=_</tt> into the
e634d33deb86 added new website
haftmann
parents:
diff changeset
   189
          equivalence sign, <tt>&lt;_</tt> into less-or-equal, <tt>[|</tt> into
e634d33deb86 added new website
haftmann
parents:
diff changeset
   190
          opening semantic brackets, and so on. For greek characters, the
e634d33deb86 added new website
haftmann
parents:
diff changeset
   191
          <code>rotate</code> command works well: to input &alpha; type
e634d33deb86 added new website
haftmann
parents:
diff changeset
   192
          <code>a</code> and then <code>C-.</code> (control and <code>.</code>).
e634d33deb86 added new website
haftmann
parents:
diff changeset
   193
          You can also display the grid-of-characters in the x-symbol menu to get
e634d33deb86 added new website
haftmann
parents:
diff changeset
   194
          an overview of the available graphical representations (not all of them
e634d33deb86 added new website
haftmann
parents:
diff changeset
   195
          already have a meaning in Isabelle, though).</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   196
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   197
</dl>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   198
      <h2>System</h2>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   199
e634d33deb86 added new website
haftmann
parents:
diff changeset
   200
    <dl class="faq">
e634d33deb86 added new website
haftmann
parents:
diff changeset
   201
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   202
      <dt>I want to generate one of those flashy LaTeX documents. How?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   203
    
16240
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   204
      <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
   205
          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
   206
          <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
   207
          create a file called <tt class="shellcmd">IsaMakefile</tt> in the current directory. Put
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
   208
          your theory file(s) into the new directory and edit the file
16240
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   209
          <tt class="shellcmd">ROOT.ML</tt> in there (following the comments) to tell Isabelle which
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
   210
          of the theories to load (and in which order). Go back to the parent
16240
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   211
          directory (where the <tt class="shellcmd">IsaMakefile</tt> is) and type <tt class="shellcmd">isatool
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
   212
          make</tt>. Isabelle should then process your theories and tell you where
e634d33deb86 added new website
haftmann
parents:
diff changeset
   213
          to find the finished document. For more information on generating
e634d33deb86 added new website
haftmann
parents:
diff changeset
   214
          documents see the Isabelle Tutorial, Chapter 4.</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   215
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   216
      <dt>I have a large formalization with many theories. Must I process all
e634d33deb86 added new website
haftmann
parents:
diff changeset
   217
          of them all of the time?</dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   218
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   219
      <dd>No, you can tell Isabelle to build a so-called heap image. This heap
e634d33deb86 added new website
haftmann
parents:
diff changeset
   220
          image can contain your preloaded theories. To get one, set up a directory
16240
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   221
          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
   222
          command <tt class="shellcmd">isatool usedir -b HOL MyImage</tt> in that directory to
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
   223
          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
   224
          should then be able to invoke Isabelle with <tt class="shellcmd">Isabelle -l MyImage</tt>
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
   225
          and have everything that is loaded in ROOT.ML instantly available.</dd>
17661
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
   226
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
   227
      <dt>Can I run Isabelle on Windows?</dt>
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
   228
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
   229
      <dd>Not really.  The Cygwin environment provides a Unixoid
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
   230
      look-and-feel that is sufficient for very basic Isabelle
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
   231
      functionality.  See also <a
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
   232
      href="installation_notes_cygwin.html">Installation notes for
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
   233
      Cygwin/Windows.</a>
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
   234
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
   235
      To try out Isabelle it might be much easier to use a Linux boot
994d010c0abd updates for Isabelle2005;
wenzelm
parents: 17563
diff changeset
   236
      CD, such as <a href="http://www.knoppix.org/">Knoppix</a>.</dd>
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
   237
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   238
    </dl>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   239
e634d33deb86 added new website
haftmann
parents:
diff changeset
   240
    </div>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   241
    <div class="hr"><hr/></div>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   242
    <?include file="//include/footer.include.html"?>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   243
</body>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   244
e634d33deb86 added new website
haftmann
parents:
diff changeset
   245
</html>