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}.