updated links to the old ftp site
authorpaulson
Tue Feb 10 12:17:04 2004 +0100 (2004-02-10)
changeset 14379ea10a8c3e9cf
parent 14378 69c4d5997669
child 14380 04b603a6f17d
updated links to the old ftp site
Admin/page/dist-content/docs.content
Admin/page/dist-content/past.content
Admin/page/main-content/index.content
doc-src/ERRATA.txt
doc-src/TutorialI/Advanced/document/Partial.tex
doc-src/TutorialI/CTL/document/CTL.tex
doc-src/TutorialI/CTL/document/CTLind.tex
doc-src/TutorialI/CTL/document/PDL.tex
doc-src/TutorialI/Documents/document/Documents.tex
doc-src/TutorialI/Inductive/document/AB.tex
doc-src/TutorialI/Inductive/document/Advanced.tex
doc-src/TutorialI/Inductive/document/Star.tex
doc-src/TutorialI/Misc/document/AdvancedInd.tex
doc-src/TutorialI/Types/document/Overloading2.tex
doc-src/TutorialI/Types/document/Records.tex
doc-src/manual.bib
doc-src/preface.tex
     1.1 --- a/Admin/page/dist-content/docs.content	Tue Feb 10 12:02:11 2004 +0100
     1.2 +++ b/Admin/page/dist-content/docs.content	Tue Feb 10 12:17:04 2004 +0100
     1.3 @@ -26,6 +26,6 @@
     1.4  
     1.5  Use the mailing list <a href="mailto:
     1.6  isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> and its
     1.7 -<a href="ftp://ftp.cl.cam.ac.uk/ml/index.html">archive</a> to discuss
     1.8 +<a href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to discuss
     1.9  problems and results.  Why not <a
    1.10  href="mailto:lcp@cl.cam.ac.uk">subscribe</a>?
     2.1 --- a/Admin/page/dist-content/past.content	Tue Feb 10 12:02:11 2004 +0100
     2.2 +++ b/Admin/page/dist-content/past.content	Tue Feb 10 12:17:04 2004 +0100
     2.3 @@ -7,15 +7,15 @@
     2.4  Past releases of Isabelle are available from the Cambrige ftp archive:
     2.5  
     2.6  <ul>
     2.7 -<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle2002.tar.gz">Isabelle2002</a></li>
     2.8 -<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle99-2.tar.gz">Isabelle99-2</a></li>
     2.9 -<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle99-1.tar.gz">Isabelle99-1</a></li>
    2.10 -<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle99.tar.gz">Isabelle99</a></li>
    2.11 -<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle98-1.tar.gz">Isabelle98-1</a></li>
    2.12 -<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle98.tar.gz">Isabelle98</a></li>
    2.13 -<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-8.tar.gz">Isabelle94-8</a></li>
    2.14 -<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-7.tar.gz">Isabelle94-7</a></li>
    2.15 -<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-6.tar.gz">Isabelle94-6</a></li>
    2.16 -<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94.tar.gz">Isabelle94</a></li>
    2.17 -<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle93.tar.gz">Isabelle93</a></li>
    2.18 +<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle2002.tar.gz">Isabelle2002</a></li>
    2.19 +<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99-2.tar.gz">Isabelle99-2</a></li>
    2.20 +<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99-1.tar.gz">Isabelle99-1</a></li>
    2.21 +<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99.tar.gz">Isabelle99</a></li>
    2.22 +<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle98-1.tar.gz">Isabelle98-1</a></li>
    2.23 +<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle98.tar.gz">Isabelle98</a></li>
    2.24 +<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-8.tar.gz">Isabelle94-8</a></li>
    2.25 +<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-7.tar.gz">Isabelle94-7</a></li>
    2.26 +<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-6.tar.gz">Isabelle94-6</a></li>
    2.27 +<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94.tar.gz">Isabelle94</a></li>
    2.28 +<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle93.tar.gz">Isabelle93</a></li>
    2.29  </ul>
     3.1 --- a/Admin/page/main-content/index.content	Tue Feb 10 12:02:11 2004 +0100
     3.2 +++ b/Admin/page/main-content/index.content	Tue Feb 10 12:17:04 2004 +0100
     3.3 @@ -67,7 +67,7 @@
     3.4  
     3.5  Use the mailing list <a href="mailto:
     3.6  isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> 
     3.7 -and its <a href="ftp://ftp.cl.cam.ac.uk/ml/index.html">archive</a> to
     3.8 +and its <a href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to
     3.9  discuss problems and results.  Why not <a
    3.10  href="mailto:lcp@cl.cam.ac.uk">subscribe</a>? 
    3.11  
     4.1 --- a/doc-src/ERRATA.txt	Tue Feb 10 12:02:11 2004 +0100
     4.2 +++ b/doc-src/ERRATA.txt	Tue Feb 10 12:17:04 2004 +0100
     4.3 @@ -122,9 +122,9 @@
     4.4  first.
     4.5  
     4.6  page 259: HOL theory files may now include datatype declarations, primitive
     4.7 -recursive function definitions, and (co)inductive definitions.  (These new
     4.8 -sections are available separately as the file ml/HOL-extensions.dvi.gz,
     4.9 -host ftp.cl.cam.ac.uk.)
    4.10 +recursive function definitions, and (co)inductive definitions.  These new
    4.11 +sections are available separately at
    4.12 +    http://www.cl.cam.ac.uk/users/lcp/archive/ml/HOL-extensions.dvi.gz
    4.13  
    4.14  page 259: now there is another examples directory, IMP (a semantics
    4.15  equivalence proof for an imperative language)
     5.1 --- a/doc-src/TutorialI/Advanced/document/Partial.tex	Tue Feb 10 12:02:11 2004 +0100
     5.2 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex	Tue Feb 10 12:17:04 2004 +0100
     5.3 @@ -212,8 +212,8 @@
     5.4  correctness of loops expressed with \isa{while}:
     5.5  \begin{isabelle}%
     5.6  \ \ \ \ \ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharsemicolon}\isanewline
     5.7 -\isaindent{\ \ \ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymnot}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\ s{\isacharsemicolon}\ wf\ r{\isacharsemicolon}\isanewline
     5.8 -\isaindent{\ \ \ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\isanewline
     5.9 +\isaindent{\ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymnot}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\ s{\isacharsemicolon}\ wf\ r{\isacharsemicolon}\isanewline
    5.10 +\isaindent{\ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\isanewline
    5.11  \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}%
    5.12  \end{isabelle} \isa{P} needs to be true of
    5.13  the initial state \isa{s} and invariant under \isa{c} (premises 1
     6.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Tue Feb 10 12:02:11 2004 +0100
     6.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Tue Feb 10 12:17:04 2004 +0100
     6.3 @@ -123,7 +123,7 @@
     6.4  \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}}{\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
     6.5  \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}{\isasymforall}t{\isachardot}\ }{\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
     6.6  \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}{\isasymforall}p{\isachardot}\ }{\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
     6.7 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ \ \ }{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
     6.8 +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ }{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
     6.9  \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
    6.10  \end{isabelle}
    6.11  Now we eliminate the disjunction. The case \isa{p\ {\isadigit{0}}\ {\isasymin}\ A} is trivial:%
    6.12 @@ -145,8 +145,8 @@
    6.13  \begin{isamarkuptxt}%
    6.14  \begin{isabelle}%
    6.15  \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\isanewline
    6.16 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ \ \ }{\isasymforall}pa{\isachardot}\ p\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ pa\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
    6.17 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ \ \ {\isasymforall}pa{\isachardot}\ }{\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
    6.18 +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ }{\isasymforall}pa{\isachardot}\ p\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ pa\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
    6.19 +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ {\isasymforall}pa{\isachardot}\ }{\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
    6.20  \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
    6.21  \end{isabelle}
    6.22  It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}}, that is, 
     7.1 --- a/doc-src/TutorialI/CTL/document/CTLind.tex	Tue Feb 10 12:02:11 2004 +0100
     7.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Tue Feb 10 12:17:04 2004 +0100
     7.3 @@ -111,9 +111,9 @@
     7.4  \noindent
     7.5  \begin{isabelle}%
     7.6  \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\isanewline
     7.7 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ \ \ }{\isasymforall}y{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline
     7.8 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ \ \ {\isasymforall}y{\isachardot}\ }y\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ y\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline
     7.9 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ \ \ }t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\isanewline
    7.10 +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ }{\isasymforall}y{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline
    7.11 +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ {\isasymforall}y{\isachardot}\ }y\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ y\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline
    7.12 +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ }t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\isanewline
    7.13  \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ }{\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
    7.14  \ {\isadigit{2}}{\isachardot}\ {\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\isanewline
    7.15  \isaindent{\ {\isadigit{2}}{\isachardot}\ }wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}%
     8.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex	Tue Feb 10 12:02:11 2004 +0100
     8.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex	Tue Feb 10 12:17:04 2004 +0100
     8.3 @@ -167,7 +167,7 @@
     8.4  \isa{converse{\isacharunderscore}rtrancl{\isacharunderscore}induct} already exists:
     8.5  \begin{isabelle}%
     8.6  \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ b{\isacharsemicolon}\isanewline
     8.7 -\isaindent{\ \ \ \ \ \ \ \ }{\isasymAnd}y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}z{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ y{\isasymrbrakk}\isanewline
     8.8 +\isaindent{\ \ \ \ \ \ }{\isasymAnd}y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}z{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ y{\isasymrbrakk}\isanewline
     8.9  \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ P\ a%
    8.10  \end{isabelle}
    8.11  It says that if \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}} and we know \isa{P\ b} then we can infer
     9.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex	Tue Feb 10 12:02:11 2004 +0100
     9.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex	Tue Feb 10 12:17:04 2004 +0100
     9.3 @@ -307,8 +307,8 @@
     9.4  \noindent The datatype induction rule generated here is of the form
     9.5    \begin{isabelle}%
     9.6  \ {\isasymlbrakk}P\ Leaf{\isacharsemicolon}\isanewline
     9.7 -\isaindent{\ \ \ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline
     9.8 -\isaindent{\ \ \ \ \ \ \ }{\isasymlbrakk}P\ bintree{\isadigit{1}}{\isacharsemicolon}\ P\ bintree{\isadigit{2}}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Branch\ a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isacharparenright}{\isasymrbrakk}\isanewline
     9.9 +\isaindent{\ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline
    9.10 +\isaindent{\ \ \ \ \ }{\isasymlbrakk}P\ bintree{\isadigit{1}}{\isacharsemicolon}\ P\ bintree{\isadigit{2}}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Branch\ a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isacharparenright}{\isasymrbrakk}\isanewline
    9.11  \isaindent{\ }{\isasymLongrightarrow}\ P\ bintree%
    9.12  \end{isabelle}%
    9.13  \end{isamarkuptext}%
    10.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex	Tue Feb 10 12:02:11 2004 +0100
    10.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex	Tue Feb 10 12:17:04 2004 +0100
    10.3 @@ -110,8 +110,7 @@
    10.4  1 on our way from 0 to 2. Formally, we appeal to the following discrete
    10.5  intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
    10.6  \begin{isabelle}%
    10.7 -\ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline
    10.8 -\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
    10.9 +\ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isacharless}n{\isachardot}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}i{\isasymle}n{\isachardot}\ f\ i\ {\isacharequal}\ k%
   10.10  \end{isabelle}
   10.11  where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
   10.12  \isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function\footnote{See
    11.1 --- a/doc-src/TutorialI/Inductive/document/Advanced.tex	Tue Feb 10 12:02:11 2004 +0100
    11.2 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex	Tue Feb 10 12:17:04 2004 +0100
    11.3 @@ -92,7 +92,7 @@
    11.4  \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}args\ f{\isachardot}\isanewline
    11.5  \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
    11.6  \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ gterms\ F\ {\isasymand}\ {\isacharparenleft}t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
    11.7 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
    11.8 +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
    11.9  \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\isanewline
   11.10  \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }Apply\ f\ args\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}%
   11.11  \end{isabelle}%
   11.12 @@ -167,7 +167,7 @@
   11.13  \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
   11.14  \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\isanewline
   11.15  \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline
   11.16 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
   11.17 +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
   11.18  \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity%
   11.19  \end{isabelle}%
   11.20  \end{isamarkuptxt}%
   11.21 @@ -201,7 +201,7 @@
   11.22  \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}}{\isasymin}\ lists\isanewline
   11.23  \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ }{\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasyminter}\isanewline
   11.24  \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ {\isacharparenleft}}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharbraceright}{\isacharparenright}{\isacharsemicolon}\isanewline
   11.25 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
   11.26 +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
   11.27  \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity%
   11.28  \end{isabelle}%
   11.29  \end{isamarkuptxt}%
    12.1 --- a/doc-src/TutorialI/Inductive/document/Star.tex	Tue Feb 10 12:02:11 2004 +0100
    12.2 +++ b/doc-src/TutorialI/Inductive/document/Star.tex	Tue Feb 10 12:17:04 2004 +0100
    12.3 @@ -63,7 +63,7 @@
    12.4  \isa{rtc{\isachardot}induct}:
    12.5  \begin{isabelle}%
    12.6  \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}{\isacharquery}xb{\isacharcomma}\ {\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharsemicolon}\isanewline
    12.7 -\isaindent{\ \ \ \ \ \ \ \ }{\isasymAnd}x\ y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isacharquery}P\ y\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ z{\isasymrbrakk}\isanewline
    12.8 +\isaindent{\ \ \ \ \ \ }{\isasymAnd}x\ y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isacharquery}P\ y\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ z{\isasymrbrakk}\isanewline
    12.9  \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}xb\ {\isacharquery}xa%
   12.10  \end{isabelle}
   12.11  It says that \isa{{\isacharquery}P} holds for an arbitrary pair \isa{{\isacharparenleft}{\isacharquery}xb{\isacharcomma}{\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}} if \isa{{\isacharquery}P} is preserved by all rules of the inductive definition,
    13.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Feb 10 12:02:11 2004 +0100
    13.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Feb 10 12:17:04 2004 +0100
    13.3 @@ -144,7 +144,7 @@
    13.4  induction, where you prove $P(n)$ under the assumption that $P(m)$
    13.5  holds for all $m<n$. In Isabelle, this is the theorem \tdx{nat_less_induct}:
    13.6  \begin{isabelle}%
    13.7 -\ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
    13.8 +\ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
    13.9  \end{isabelle}
   13.10  As an application, we prove a property of the following
   13.11  function:%
   13.12 @@ -184,8 +184,7 @@
   13.13  \noindent
   13.14  We get the following proof state:
   13.15  \begin{isabelle}%
   13.16 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
   13.17 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ }{\isasymforall}i{\isachardot}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
   13.18 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i\ {\isasymLongrightarrow}\ {\isasymforall}i{\isachardot}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
   13.19  \end{isabelle}
   13.20  After stripping the \isa{{\isasymforall}i}, the proof continues with a case
   13.21  distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isadigit{0}}} is trivial and we focus on
   13.22 @@ -201,8 +200,7 @@
   13.23  \begin{isamarkuptxt}%
   13.24  \begin{isabelle}%
   13.25  \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ i\ nat{\isachardot}\isanewline
   13.26 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharparenright}{\isacharsemicolon}\ i\ {\isacharequal}\ Suc\ nat{\isasymrbrakk}\isanewline
   13.27 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
   13.28 +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharsemicolon}\ i\ {\isacharequal}\ Suc\ nat{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
   13.29  \end{isabelle}%
   13.30  \end{isamarkuptxt}%
   13.31  \isamarkuptrue%
    14.1 --- a/doc-src/TutorialI/Types/document/Overloading2.tex	Tue Feb 10 12:02:11 2004 +0100
    14.2 +++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Tue Feb 10 12:17:04 2004 +0100
    14.3 @@ -41,16 +41,14 @@
    14.4  defined on all numeric types and sometimes on other types as well, for example
    14.5  $-$ and \isa{{\isasymle}} on sets.
    14.6  
    14.7 -In addition there is a special input syntax for bounded quantifiers:
    14.8 +In addition there is a special syntax for bounded quantifiers:
    14.9  \begin{center}
   14.10  \begin{tabular}{lcl}
   14.11 -\isa{{\isasymforall}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymrightharpoonup}} & \isa{{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x} \\
   14.12 -\isa{{\isasymexists}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymrightharpoonup}} & \isa{{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x}
   14.13 +\isa{{\isasymforall}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x{\isachardoublequote}} \\
   14.14 +\isa{{\isasymexists}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x{\isachardoublequote}}
   14.15  \end{tabular}
   14.16  \end{center}
   14.17 -And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.
   14.18 -The form on the left is translated into the one on the right upon input.
   14.19 -For technical reasons, it is not translated back upon output.%
   14.20 +And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.%
   14.21  \end{isamarkuptext}%
   14.22  \isamarkuptrue%
   14.23  \isamarkupfalse%
    15.1 --- a/doc-src/TutorialI/Types/document/Records.tex	Tue Feb 10 12:02:11 2004 +0100
    15.2 +++ b/doc-src/TutorialI/Types/document/Records.tex	Tue Feb 10 12:17:04 2004 +0100
    15.3 @@ -319,7 +319,7 @@
    15.4  \begin{isabelle}%
    15.5  \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}Xcoord\ Ycoord\ more{\isachardot}\isanewline
    15.6  \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}{\isacharsemicolon}\isanewline
    15.7 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}{\isasymrbrakk}\isanewline
    15.8 +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}{\isasymrbrakk}\isanewline
    15.9  \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}%
   15.10  \end{isabelle} Again, \isa{simp} finishes the proof.  Because \isa{r} is now represented as
   15.11    an explicit record construction, the updates can be applied and the
    16.1 --- a/doc-src/manual.bib	Tue Feb 10 12:02:11 2004 +0100
    16.2 +++ b/doc-src/manual.bib	Tue Feb 10 12:17:04 2004 +0100
    16.3 @@ -937,7 +937,7 @@
    16.4    number	= 3,
    16.5    pages		= {353-389},
    16.6    year		= 1993,
    16.7 -  url		= {\url{ftp://ftp.cl.cam.ac.uk/ml/set-I.ps.gz}}}
    16.8 +  url		= {\url{http://www.cl.cam.ac.uk/users/lcp/papers/Sets/set-I.pdf}}
    16.9  
   16.10  @Article{paulson-set-II,
   16.11    author	= {Lawrence C. Paulson},
    17.1 --- a/doc-src/preface.tex	Tue Feb 10 12:02:11 2004 +0100
    17.2 +++ b/doc-src/preface.tex	Tue Feb 10 12:17:04 2004 +0100
    17.3 @@ -104,16 +104,10 @@
    17.4  graphical user interface, and developments in the standard object-logics.
    17.5  I hope but cannot promise to maintain upwards compatibility.
    17.6  
    17.7 -Isabelle is available by anonymous ftp:
    17.8 -\begin{itemize}
    17.9 -\item University of Cambridge\\
   17.10 -        host {\tt ftp.cl.cam.ac.uk}\\
   17.11 -        directory {\tt ml}
   17.12 -
   17.13 -\item Technical University of Munich\\
   17.14 -        host {\tt ftp.informatik.tu-muenchen.de}\\
   17.15 -        directory {\tt local/lehrstuhl/nipkow}
   17.16 -\end{itemize}
   17.17 +Isabelle can be downloaded from .
   17.18 +\begin{quote}
   17.19 +{\tt http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/}  
   17.20 +\end{quote}
   17.21  The electronic distribution list {\tt isabelle-users\at cl.cam.ac.uk}
   17.22  provides a forum for discussing problems and applications involving
   17.23  Isabelle.  To join, send me a message via {\tt lcp\at cl.cam.ac.uk}.