--- a/Admin/page/dist-content/docs.content Tue Feb 10 12:02:11 2004 +0100
+++ b/Admin/page/dist-content/docs.content Tue Feb 10 12:17:04 2004 +0100
@@ -26,6 +26,6 @@
Use the mailing list <a href="mailto:
isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> and its
-<a href="ftp://ftp.cl.cam.ac.uk/ml/index.html">archive</a> to discuss
+<a href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to discuss
problems and results. Why not <a
href="mailto:lcp@cl.cam.ac.uk">subscribe</a>?
--- a/Admin/page/dist-content/past.content Tue Feb 10 12:02:11 2004 +0100
+++ b/Admin/page/dist-content/past.content Tue Feb 10 12:17:04 2004 +0100
@@ -7,15 +7,15 @@
Past releases of Isabelle are available from the Cambrige ftp archive:
<ul>
-<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle2002.tar.gz">Isabelle2002</a></li>
-<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle99-2.tar.gz">Isabelle99-2</a></li>
-<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle99-1.tar.gz">Isabelle99-1</a></li>
-<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle99.tar.gz">Isabelle99</a></li>
-<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle98-1.tar.gz">Isabelle98-1</a></li>
-<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle98.tar.gz">Isabelle98</a></li>
-<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-8.tar.gz">Isabelle94-8</a></li>
-<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-7.tar.gz">Isabelle94-7</a></li>
-<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-6.tar.gz">Isabelle94-6</a></li>
-<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94.tar.gz">Isabelle94</a></li>
-<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle93.tar.gz">Isabelle93</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle2002.tar.gz">Isabelle2002</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99-2.tar.gz">Isabelle99-2</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99-1.tar.gz">Isabelle99-1</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99.tar.gz">Isabelle99</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle98-1.tar.gz">Isabelle98-1</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle98.tar.gz">Isabelle98</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-8.tar.gz">Isabelle94-8</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-7.tar.gz">Isabelle94-7</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-6.tar.gz">Isabelle94-6</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94.tar.gz">Isabelle94</a></li>
+<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle93.tar.gz">Isabelle93</a></li>
</ul>
--- a/Admin/page/main-content/index.content Tue Feb 10 12:02:11 2004 +0100
+++ b/Admin/page/main-content/index.content Tue Feb 10 12:17:04 2004 +0100
@@ -67,7 +67,7 @@
Use the mailing list <a href="mailto:
isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>
-and its <a href="ftp://ftp.cl.cam.ac.uk/ml/index.html">archive</a> to
+and its <a href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to
discuss problems and results. Why not <a
href="mailto:lcp@cl.cam.ac.uk">subscribe</a>?
--- a/doc-src/ERRATA.txt Tue Feb 10 12:02:11 2004 +0100
+++ b/doc-src/ERRATA.txt Tue Feb 10 12:17:04 2004 +0100
@@ -122,9 +122,9 @@
first.
page 259: HOL theory files may now include datatype declarations, primitive
-recursive function definitions, and (co)inductive definitions. (These new
-sections are available separately as the file ml/HOL-extensions.dvi.gz,
-host ftp.cl.cam.ac.uk.)
+recursive function definitions, and (co)inductive definitions. These new
+sections are available separately at
+ http://www.cl.cam.ac.uk/users/lcp/archive/ml/HOL-extensions.dvi.gz
page 259: now there is another examples directory, IMP (a semantics
equivalence proof for an imperative language)
--- a/doc-src/TutorialI/Advanced/document/Partial.tex Tue Feb 10 12:02:11 2004 +0100
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex Tue Feb 10 12:17:04 2004 +0100
@@ -212,8 +212,8 @@
correctness of loops expressed with \isa{while}:
\begin{isabelle}%
\ \ \ \ \ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharsemicolon}\isanewline
-\isaindent{\ \ \ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymnot}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\ s{\isacharsemicolon}\ wf\ r{\isacharsemicolon}\isanewline
-\isaindent{\ \ \ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\isanewline
+\isaindent{\ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymnot}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\ s{\isacharsemicolon}\ wf\ r{\isacharsemicolon}\isanewline
+\isaindent{\ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\isanewline
\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}%
\end{isabelle} \isa{P} needs to be true of
the initial state \isa{s} and invariant under \isa{c} (premises 1
--- a/doc-src/TutorialI/CTL/document/CTL.tex Tue Feb 10 12:02:11 2004 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Tue Feb 10 12:17:04 2004 +0100
@@ -123,7 +123,7 @@
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}}{\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
\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
\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
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ \ \ }{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ }{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
\end{isabelle}
Now we eliminate the disjunction. The case \isa{p\ {\isadigit{0}}\ {\isasymin}\ A} is trivial:%
@@ -145,8 +145,8 @@
\begin{isamarkuptxt}%
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\isanewline
-\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
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ \ \ {\isasymforall}pa{\isachardot}\ }{\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
+\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
+\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ {\isasymforall}pa{\isachardot}\ }{\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
\end{isabelle}
It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}}, that is,
--- a/doc-src/TutorialI/CTL/document/CTLind.tex Tue Feb 10 12:02:11 2004 +0100
+++ b/doc-src/TutorialI/CTL/document/CTLind.tex Tue Feb 10 12:17:04 2004 +0100
@@ -111,9 +111,9 @@
\noindent
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ \ \ }{\isasymforall}y{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline
-\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
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ \ \ }t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ }{\isasymforall}y{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline
+\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
+\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ }t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ }{\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
\ {\isadigit{2}}{\isachardot}\ {\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\isanewline
\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}%
--- a/doc-src/TutorialI/CTL/document/PDL.tex Tue Feb 10 12:02:11 2004 +0100
+++ b/doc-src/TutorialI/CTL/document/PDL.tex Tue Feb 10 12:17:04 2004 +0100
@@ -167,7 +167,7 @@
\isa{converse{\isacharunderscore}rtrancl{\isacharunderscore}induct} already exists:
\begin{isabelle}%
\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ b{\isacharsemicolon}\isanewline
-\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
+\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
\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ P\ a%
\end{isabelle}
It says that if \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}} and we know \isa{P\ b} then we can infer
--- a/doc-src/TutorialI/Documents/document/Documents.tex Tue Feb 10 12:02:11 2004 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Tue Feb 10 12:17:04 2004 +0100
@@ -307,8 +307,8 @@
\noindent The datatype induction rule generated here is of the form
\begin{isabelle}%
\ {\isasymlbrakk}P\ Leaf{\isacharsemicolon}\isanewline
-\isaindent{\ \ \ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline
-\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
+\isaindent{\ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline
+\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
\isaindent{\ }{\isasymLongrightarrow}\ P\ bintree%
\end{isabelle}%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/Inductive/document/AB.tex Tue Feb 10 12:02:11 2004 +0100
+++ b/doc-src/TutorialI/Inductive/document/AB.tex Tue Feb 10 12:17:04 2004 +0100
@@ -110,8 +110,7 @@
1 on our way from 0 to 2. Formally, we appeal to the following discrete
intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
\begin{isabelle}%
-\ \ \ \ \ {\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
-\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
+\ \ \ \ \ {\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%
\end{isabelle}
where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
\isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function\footnote{See
--- a/doc-src/TutorialI/Inductive/document/Advanced.tex Tue Feb 10 12:02:11 2004 +0100
+++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Tue Feb 10 12:17:04 2004 +0100
@@ -92,7 +92,7 @@
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}args\ f{\isachardot}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
\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
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }Apply\ f\ args\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}%
\end{isabelle}%
@@ -167,7 +167,7 @@
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity%
\end{isabelle}%
\end{isamarkuptxt}%
@@ -201,7 +201,7 @@
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}}{\isasymin}\ lists\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ }{\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasyminter}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ {\isacharparenleft}}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharbraceright}{\isacharparenright}{\isacharsemicolon}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity%
\end{isabelle}%
\end{isamarkuptxt}%
--- a/doc-src/TutorialI/Inductive/document/Star.tex Tue Feb 10 12:02:11 2004 +0100
+++ b/doc-src/TutorialI/Inductive/document/Star.tex Tue Feb 10 12:17:04 2004 +0100
@@ -63,7 +63,7 @@
\isa{rtc{\isachardot}induct}:
\begin{isabelle}%
\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}{\isacharquery}xb{\isacharcomma}\ {\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharsemicolon}\isanewline
-\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
+\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
\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}xb\ {\isacharquery}xa%
\end{isabelle}
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,
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Feb 10 12:02:11 2004 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Feb 10 12:17:04 2004 +0100
@@ -144,7 +144,7 @@
induction, where you prove $P(n)$ under the assumption that $P(m)$
holds for all $m<n$. In Isabelle, this is the theorem \tdx{nat_less_induct}:
\begin{isabelle}%
-\ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
+\ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
\end{isabelle}
As an application, we prove a property of the following
function:%
@@ -184,8 +184,7 @@
\noindent
We get the following proof state:
\begin{isabelle}%
-\ {\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
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ }{\isasymforall}i{\isachardot}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
+\ {\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%
\end{isabelle}
After stripping the \isa{{\isasymforall}i}, the proof continues with a case
distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isadigit{0}}} is trivial and we focus on
@@ -201,8 +200,7 @@
\begin{isamarkuptxt}%
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ i\ nat{\isachardot}\isanewline
-\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
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
+\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%
\end{isabelle}%
\end{isamarkuptxt}%
\isamarkuptrue%
--- a/doc-src/TutorialI/Types/document/Overloading2.tex Tue Feb 10 12:02:11 2004 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex Tue Feb 10 12:17:04 2004 +0100
@@ -41,16 +41,14 @@
defined on all numeric types and sometimes on other types as well, for example
$-$ and \isa{{\isasymle}} on sets.
-In addition there is a special input syntax for bounded quantifiers:
+In addition there is a special syntax for bounded quantifiers:
\begin{center}
\begin{tabular}{lcl}
-\isa{{\isasymforall}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymrightharpoonup}} & \isa{{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x} \\
-\isa{{\isasymexists}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymrightharpoonup}} & \isa{{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x}
+\isa{{\isasymforall}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x{\isachardoublequote}} \\
+\isa{{\isasymexists}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x{\isachardoublequote}}
\end{tabular}
\end{center}
-And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.
-The form on the left is translated into the one on the right upon input.
-For technical reasons, it is not translated back upon output.%
+And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
--- a/doc-src/TutorialI/Types/document/Records.tex Tue Feb 10 12:02:11 2004 +0100
+++ b/doc-src/TutorialI/Types/document/Records.tex Tue Feb 10 12:17:04 2004 +0100
@@ -319,7 +319,7 @@
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}Xcoord\ Ycoord\ more{\isachardot}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}{\isacharsemicolon}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}{\isasymrbrakk}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}{\isasymrbrakk}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}%
\end{isabelle} Again, \isa{simp} finishes the proof. Because \isa{r} is now represented as
an explicit record construction, the updates can be applied and the
--- a/doc-src/manual.bib Tue Feb 10 12:02:11 2004 +0100
+++ b/doc-src/manual.bib Tue Feb 10 12:17:04 2004 +0100
@@ -937,7 +937,7 @@
number = 3,
pages = {353-389},
year = 1993,
- url = {\url{ftp://ftp.cl.cam.ac.uk/ml/set-I.ps.gz}}}
+ url = {\url{http://www.cl.cam.ac.uk/users/lcp/papers/Sets/set-I.pdf}}
@Article{paulson-set-II,
author = {Lawrence C. Paulson},
--- a/doc-src/preface.tex Tue Feb 10 12:02:11 2004 +0100
+++ b/doc-src/preface.tex Tue Feb 10 12:17:04 2004 +0100
@@ -104,16 +104,10 @@
graphical user interface, and developments in the standard object-logics.
I hope but cannot promise to maintain upwards compatibility.
-Isabelle is available by anonymous ftp:
-\begin{itemize}
-\item University of Cambridge\\
- host {\tt ftp.cl.cam.ac.uk}\\
- directory {\tt ml}
-
-\item Technical University of Munich\\
- host {\tt ftp.informatik.tu-muenchen.de}\\
- directory {\tt local/lehrstuhl/nipkow}
-\end{itemize}
+Isabelle can be downloaded from .
+\begin{quote}
+{\tt http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/}
+\end{quote}
The electronic distribution list {\tt isabelle-users\at cl.cam.ac.uk}
provides a forum for discussing problems and applications involving
Isabelle. To join, send me a message via {\tt lcp\at cl.cam.ac.uk}.