--- a/doc-src/IsarRef/intro.tex Wed Sep 21 18:04:49 2005 +0200
+++ b/doc-src/IsarRef/intro.tex Wed Sep 21 18:06:04 2005 +0200
@@ -60,11 +60,11 @@
anything with Isabelle/Isar is as follows:
\begin{ttbox}
isabelle -I HOL\medskip
-\out{> Welcome to Isabelle/HOL (Isabelle2002)}\medskip
-theory Foo = Main:
+\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
+theory Foo imports Main begin;
constdefs foo :: nat "foo == 1";
lemma "0 < foo" by (simp add: foo_def);
-end
+end;
\end{ttbox}
Note that any Isabelle/Isar command may be retracted by \texttt{undo}. See
the Isabelle/Isar Quick Reference (appendix~\ref{ap:refcard}) for a
--- a/doc-src/Locales/Locales/Locales.thy Wed Sep 21 18:04:49 2005 +0200
+++ b/doc-src/Locales/Locales/Locales.thy Wed Sep 21 18:06:04 2005 +0200
@@ -8,7 +8,7 @@
(*<*)
theory Locales imports Main begin
-ML_setup {* print_mode := "type_brackets" :: !print_mode; *}
+ML {* print_mode := "type_brackets" :: !print_mode; *}
(*>*)
section {* Overview *}
@@ -35,7 +35,7 @@
Wenzel~\cite{Wenzel2002a}. Subsequently, Wenzel re-implemented
locales for
the new proof format. The implementation, available with
- Isabelle2003, constitutes a complete re-design and exploits that
+ Isabelle2002 or later, constitutes a complete re-design and exploits that
both Isar and locales are based on the notion of context,
and thus locales are seen as a natural extension of Isar.
Nevertheless, locales can also be used with proof scripts:
--- a/doc-src/Locales/Locales/document/Locales.tex Wed Sep 21 18:04:49 2005 +0200
+++ b/doc-src/Locales/Locales/document/Locales.tex Wed Sep 21 18:06:04 2005 +0200
@@ -55,7 +55,7 @@
Wenzel~\cite{Wenzel2002a}. Subsequently, Wenzel re-implemented
locales for
the new proof format. The implementation, available with
- Isabelle2003, constitutes a complete re-design and exploits that
+ Isabelle2002 or later, constitutes a complete re-design and exploits that
both Isar and locales are based on the notion of context,
and thus locales are seen as a natural extension of Isar.
Nevertheless, locales can also be used with proof scripts:
--- a/doc-src/System/misc.tex Wed Sep 21 18:04:49 2005 +0200
+++ b/doc-src/System/misc.tex Wed Sep 21 18:06:04 2005 +0200
@@ -279,7 +279,7 @@
\section{Output the version identifier of the Isabelle distribution --- \texttt{isatool version}}
The \tooldx{version} utility outputs the version identifier of the Isabelle
-distribution being used, e.g.\ \texttt{Isabelle2004}. There are no options
+distribution being used, e.g.\ \texttt{Isabelle2005}. There are no options
nor arguments.
%%% Local Variables: