# HG changeset patch
# User wenzelm
# Date 1127318764 -7200
# Node ID 20c0b69dd1927d4d005f798af9dda7f156a000e2
# Parent  484ff733f29ce8d265257d030f12498bcb1d912c
updated for Isabelle2005;

diff -r 484ff733f29c -r 20c0b69dd192 doc-src/IsarRef/intro.tex
--- 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
diff -r 484ff733f29c -r 20c0b69dd192 doc-src/Locales/Locales/Locales.thy
--- 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:
diff -r 484ff733f29c -r 20c0b69dd192 doc-src/Locales/Locales/document/Locales.tex
--- 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:
diff -r 484ff733f29c -r 20c0b69dd192 doc-src/System/misc.tex
--- 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: