# HG changeset patch
# User wenzelm
# Date 1291552978 -3600
# Node ID 482a8334ee9ef86e3f55816aafa34b2dd8ec6553
# Parent  08939f7b62622f4caf3415d6d01fc0b79ef957f6
prefer 'notepad' over 'example_proof';

diff -r 08939f7b6262 -r 482a8334ee9e doc-src/IsarImplementation/Thy/Isar.thy
--- a/doc-src/IsarImplementation/Thy/Isar.thy	Sun Dec 05 08:34:02 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Isar.thy	Sun Dec 05 13:42:58 2010 +0100
@@ -162,7 +162,8 @@
 
 text %mlex {* The following example peeks at a certain goal configuration. *}
 
-example_proof
+notepad
+begin
   have A and B and C
     ML_val {*
       val n = Thm.nprems_of (#goal @{Isar.goal});
@@ -364,7 +365,8 @@
   tactic} (abstracted over @{ML_text facts}).  This allows immediate
   experimentation without parsing of concrete syntax. *}
 
-example_proof
+notepad
+begin
   assume a: A and b: B
 
   have "A \<and> B"
@@ -379,7 +381,7 @@
     apply (tactic {* Method.insert_tac facts 1 *})
     apply (tactic {* (rtac @{thm conjI} THEN_ALL_NEW atac) 1 *})
     done
-qed
+end
 
 text {* \medskip The next example implements a method that simplifies
   the first subgoal by rewrite rules given as arguments.  *}
@@ -411,12 +413,13 @@
   this:
 *}
 
-example_proof
+notepad
+begin
   fix a b c
   assume a: "a = b"
   assume b: "b = c"
   have "a = c" by (my_simp a b)
-qed
+end
 
 text {* Here is a similar method that operates on all subgoals,
   instead of just the first one. *}
@@ -429,13 +432,13 @@
           (HOL_basic_ss addsimps thms)))))
 *} "rewrite all subgoals by given rules"
 
-example_proof
+notepad
+begin
   fix a b c
   assume a: "a = b"
   assume b: "b = c"
   have "a = c" and "c = b" by (my_simp_all a b)
-
-qed
+end
 
 text {* \medskip Apart from explicit arguments, common proof methods
   typically work with a default configuration provided by the context.
@@ -468,12 +471,13 @@
   like this:
 *}
 
-example_proof
+notepad
+begin
   fix a b c
   assume [my_simp]: "a \<equiv> b"
   assume [my_simp]: "b \<equiv> c"
   have "a \<equiv> c" by my_simp'
-qed
+end
 
 text {* \medskip The @{method my_simp} variants defined above are
   ``simple'' methods, i.e.\ the goal facts are merely inserted as goal
diff -r 08939f7b6262 -r 482a8334ee9e doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Sun Dec 05 08:34:02 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Sun Dec 05 13:42:58 2010 +0100
@@ -574,13 +574,14 @@
   the whole proof body, ignoring the block structure.
 *}
 
-example_proof
+notepad
+begin
   ML_prf %"ML" {* val a = 1 *}
   {
     ML_prf %"ML" {* val b = a + 1 *}
   } -- {* Isar block structure ignored by ML environment *}
   ML_prf %"ML" {* val c = b + 1 *}
-qed
+end
 
 text {* By side-stepping the normal scoping rules for Isar proof
   blocks, embedded ML code can refer to the different contexts and
@@ -599,10 +600,11 @@
 ML_val {* factorial 100 *}
 ML_command {* writeln (string_of_int (factorial 100)) *}
 
-example_proof
+notepad
+begin
   ML_val {* factorial 100 *}  (* FIXME check/fix indentation *)
   ML_command {* writeln (string_of_int (factorial 100)) *}
-qed
+end
 
 
 subsection {* Compile-time context *}
diff -r 08939f7b6262 -r 482a8334ee9e doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Dec 05 08:34:02 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Dec 05 13:42:58 2010 +0100
@@ -567,7 +567,8 @@
 declare [[show_types = false]]
   -- {* declaration within (local) theory context *}
 
-example_proof
+notepad
+begin
   note [[show_types = true]]
     -- {* declaration within proof (forward mode) *}
   term x
@@ -576,7 +577,7 @@
     using [[show_types = false]]
       -- {* declaration within proof (backward mode) *}
     ..
-qed
+end
 
 text {* Configuration options that are not set explicitly hold a
   default value that can depend on the application context.  This
@@ -646,13 +647,14 @@
 
 ML_val {* @{assert} (Config.get @{context} my_flag = true) *}
 
-example_proof
+notepad
+begin
   {
     note [[my_flag = false]]
     ML_val {* @{assert} (Config.get @{context} my_flag = false) *}
   }
   ML_val {* @{assert} (Config.get @{context} my_flag = true) *}
-qed
+end
 
 text {* Here is another example involving ML type @{ML_type real}
   (floating-point numbers). *}
diff -r 08939f7b6262 -r 482a8334ee9e doc-src/IsarImplementation/Thy/Proof.thy
--- a/doc-src/IsarImplementation/Thy/Proof.thy	Sun Dec 05 08:34:02 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Proof.thy	Sun Dec 05 13:42:58 2010 +0100
@@ -58,7 +58,8 @@
   The following Isar source text illustrates this scenario.
 *}
 
-example_proof
+notepad
+begin
   {
     fix x  -- {* all potential occurrences of some @{text "x::\<tau>"} are fixed *}
     {
@@ -68,7 +69,7 @@
     thm this  -- {* result still with fixed type @{text "'a"} *}
   }
   thm this  -- {* fully general result for arbitrary @{text "?x::?'a"} *}
-qed
+end
 
 text {* The Isabelle/Isar proof context manages the details of term
   vs.\ type variables, with high-level principles for moving the
@@ -199,7 +200,8 @@
   Recall that within a proof body the system always invents fresh
   ``skolem constants'', e.g.\ as follows: *}
 
-example_proof
+notepad
+begin
   ML_prf %"ML" {*
     val ctxt0 = @{context};
 
@@ -210,7 +212,7 @@
     val ([y1, y2], ctxt4) =
       ctxt3 |> Variable.variant_fixes ["y", "y"];
   *}
-  oops
+end
 
 text {* In this situation @{ML Variable.add_fixes} and @{ML
   Variable.variant_fixes} are very similar, but identical name
@@ -451,7 +453,8 @@
 text %mlex {* The following minimal example illustrates how to access
   the focus information of a structured goal state. *}
 
-example_proof
+notepad
+begin
   fix A B C :: "'a \<Rightarrow> bool"
 
   have "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
@@ -468,7 +471,8 @@
 text {* \medskip The next example demonstrates forward-elimination in
   a local context, using @{ML Obtain.result}.  *}
 
-example_proof
+notepad
+begin
   assume ex: "\<exists>x. B x"
 
   ML_prf %"ML" {*
@@ -483,6 +487,6 @@
     ProofContext.export ctxt1 ctxt0 [Thm.reflexive x]
       handle ERROR msg => (warning msg; []);
   *}
-qed
+end
 
 end
diff -r 08939f7b6262 -r 482a8334ee9e doc-src/IsarImplementation/Thy/document/Isar.tex
--- a/doc-src/IsarImplementation/Thy/document/Isar.tex	Sun Dec 05 08:34:02 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Isar.tex	Sun Dec 05 13:42:58 2010 +0100
@@ -222,8 +222,9 @@
 \isadelimmlex
 %
 \endisadelimmlex
-\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}\isamarkupfalse%
+\isacommand{notepad}\isamarkupfalse%
 \isanewline
+\isakeyword{begin}\isanewline
 %
 \isadelimproof
 \ \ %
@@ -500,8 +501,9 @@
 \isadelimmlex
 %
 \endisadelimmlex
-\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}\isamarkupfalse%
+\isacommand{notepad}\isamarkupfalse%
 \isanewline
+\isakeyword{begin}\isanewline
 %
 \isadelimproof
 \ \ %
@@ -569,15 +571,15 @@
 \endisaantiq
 \ THEN{\isaliteral{5F}{\isacharunderscore}}ALL{\isaliteral{5F}{\isacharunderscore}}NEW\ atac{\isaliteral{29}{\isacharparenright}}\ {\isadigit{1}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
 \ \ \ \ \isacommand{done}\isamarkupfalse%
-\isanewline
-\isacommand{qed}\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof
+\isanewline
 %
 \endisadelimproof
+\isacommand{end}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \medskip The next example implements a method that simplifies
@@ -624,8 +626,9 @@
   this:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}\isamarkupfalse%
+\isacommand{notepad}\isamarkupfalse%
 \isanewline
+\isakeyword{begin}\isanewline
 %
 \isadelimproof
 \ \ %
@@ -640,15 +643,15 @@
 \ b{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}b\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \isacommand{have}\isamarkupfalse%
 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}my{\isaliteral{5F}{\isacharunderscore}}simp\ a\ b{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
+\ {\isaliteral{28}{\isacharparenleft}}my{\isaliteral{5F}{\isacharunderscore}}simp\ a\ b{\isaliteral{29}{\isacharparenright}}%
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof
+\isanewline
 %
 \endisadelimproof
+\isacommand{end}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 Here is a similar method that operates on all subgoals,
@@ -677,8 +680,9 @@
 \endisadelimML
 \isanewline
 \isanewline
-\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}\isamarkupfalse%
+\isacommand{notepad}\isamarkupfalse%
 \isanewline
+\isakeyword{begin}\isanewline
 %
 \isadelimproof
 \ \ %
@@ -693,16 +697,15 @@
 \ b{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}b\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \isacommand{have}\isamarkupfalse%
 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}c\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}my{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{5F}{\isacharunderscore}}all\ a\ b{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
+\ {\isaliteral{28}{\isacharparenleft}}my{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{5F}{\isacharunderscore}}all\ a\ b{\isaliteral{29}{\isacharparenright}}%
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof
+\isanewline
 %
 \endisadelimproof
+\isacommand{end}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \medskip Apart from explicit arguments, common proof methods
@@ -765,8 +768,9 @@
   like this:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}\isamarkupfalse%
+\isacommand{notepad}\isamarkupfalse%
 \isanewline
+\isakeyword{begin}\isanewline
 %
 \isadelimproof
 \ \ %
@@ -781,15 +785,15 @@
 \ {\isaliteral{5B}{\isacharbrackleft}}my{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}b\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \ \ \isacommand{have}\isamarkupfalse%
 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ my{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{27}{\isacharprime}}\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
+\ my{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{27}{\isacharprime}}%
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof
+\isanewline
 %
 \endisadelimproof
+\isacommand{end}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \medskip The \hyperlink{method.my-simp}{\mbox{\isa{my{\isaliteral{5F}{\isacharunderscore}}simp}}} variants defined above are
diff -r 08939f7b6262 -r 482a8334ee9e doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Sun Dec 05 08:34:02 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Sun Dec 05 13:42:58 2010 +0100
@@ -630,8 +630,9 @@
   the whole proof body, ignoring the block structure.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}\isamarkupfalse%
+\isacommand{notepad}\isamarkupfalse%
 \isanewline
+\isakeyword{begin}\isanewline
 %
 \isadelimML
 \ \ %
@@ -651,7 +652,7 @@
 \isanewline
 \ \ \isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}\isamarkupfalse%
 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ val\ c\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
-\isacommand{qed}\isamarkupfalse%
+\isacommand{end}\isamarkupfalse%
 %
 \endisatagML
 {\isafoldML}%
@@ -694,8 +695,9 @@
 \endisadelimML
 \isanewline
 \isanewline
-\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}\isamarkupfalse%
+\isacommand{notepad}\isamarkupfalse%
 \isanewline
+\isakeyword{begin}\isanewline
 %
 \isadelimML
 \ \ %
@@ -713,20 +715,7 @@
 \isanewline
 %
 \endisadelimML
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
+\isacommand{end}\isamarkupfalse%
 %
 \isamarkupsubsection{Compile-time context%
 }
diff -r 08939f7b6262 -r 482a8334ee9e doc-src/IsarImplementation/Thy/document/Prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sun Dec 05 08:34:02 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sun Dec 05 13:42:58 2010 +0100
@@ -717,8 +717,9 @@
 }
 \isanewline
 \isanewline
-\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}\isamarkupfalse%
+\isacommand{notepad}\isamarkupfalse%
 \isanewline
+\isakeyword{begin}\isanewline
 %
 \isadelimproof
 \ \ %
@@ -756,15 +757,15 @@
 }
 \isanewline
 \ \ \ \ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
-\isanewline
-\isacommand{qed}\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof
+\isanewline
 %
 \endisadelimproof
+\isacommand{end}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 Configuration options that are not set explicitly hold a
@@ -925,8 +926,9 @@
 %
 \endisadelimML
 \isanewline
-\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}\isamarkupfalse%
+\isacommand{notepad}\isamarkupfalse%
 \isanewline
+\isakeyword{begin}\isanewline
 %
 \isadelimproof
 \ \ %
@@ -1005,20 +1007,7 @@
 \isanewline
 %
 \endisadelimML
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
+\isacommand{end}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 Here is another example involving ML type \verb|real|
diff -r 08939f7b6262 -r 482a8334ee9e doc-src/IsarImplementation/Thy/document/Proof.tex
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex	Sun Dec 05 08:34:02 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex	Sun Dec 05 13:42:58 2010 +0100
@@ -72,8 +72,9 @@
   The following Isar source text illustrates this scenario.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}\isamarkupfalse%
+\isacommand{notepad}\isamarkupfalse%
 \isanewline
+\isakeyword{begin}\isanewline
 %
 \isadelimproof
 \ \ %
@@ -130,20 +131,7 @@
 \isamarkupcmt{fully general result for arbitrary \isa{{\isaliteral{3F}{\isacharquery}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{27}{\isacharprime}}a}%
 }
 \isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
+\isacommand{end}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 The Isabelle/Isar proof context manages the details of term
@@ -338,8 +326,9 @@
   ``skolem constants'', e.g.\ as follows:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}\isamarkupfalse%
+\isacommand{notepad}\isamarkupfalse%
 \isanewline
+\isakeyword{begin}\isanewline
 %
 \isadelimML
 \ \ %
@@ -361,7 +350,7 @@
 \ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}y{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ y{\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ ctxt{\isadigit{4}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
 \ \ \ \ \ \ ctxt{\isadigit{3}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ Variable{\isaliteral{2E}{\isachardot}}variant{\isaliteral{5F}{\isacharunderscore}}fixes\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}y{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}y{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
-\ \ \isacommand{oops}\isamarkupfalse%
+\isacommand{end}\isamarkupfalse%
 %
 \endisatagML
 {\isafoldML}%
@@ -685,8 +674,9 @@
 \isadelimmlex
 %
 \endisadelimmlex
-\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}\isamarkupfalse%
+\isacommand{notepad}\isamarkupfalse%
 \isanewline
+\isakeyword{begin}\isanewline
 %
 \isadelimproof
 \ \ %
@@ -751,8 +741,9 @@
   a local context, using \verb|Obtain.result|.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}\isamarkupfalse%
+\isacommand{notepad}\isamarkupfalse%
 \isanewline
+\isakeyword{begin}\isanewline
 %
 \isadelimproof
 \ \ %
@@ -806,7 +797,7 @@
 \ \ \ \ ProofContext{\isaliteral{2E}{\isachardot}}export\ ctxt{\isadigit{1}}\ ctxt{\isadigit{0}}\ {\isaliteral{5B}{\isacharbrackleft}}Thm{\isaliteral{2E}{\isachardot}}reflexive\ x{\isaliteral{5D}{\isacharbrackright}}\isanewline
 \ \ \ \ \ \ handle\ ERROR\ msg\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}warning\ msg{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
-\isacommand{qed}\isamarkupfalse%
+\isacommand{end}\isamarkupfalse%
 %
 \endisatagML
 {\isafoldML}%
diff -r 08939f7b6262 -r 482a8334ee9e doc-src/IsarRef/Thy/Framework.thy
--- a/doc-src/IsarRef/Thy/Framework.thy	Sun Dec 05 08:34:02 2010 +0100
+++ b/doc-src/IsarRef/Thy/Framework.thy	Sun Dec 05 13:42:58 2010 +0100
@@ -79,12 +79,13 @@
 text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
 
 (*<*)
-example_proof
+notepad
+begin
 (*>*)
     assume "x \<in> A" and "x \<in> B"
     then have "x \<in> A \<inter> B" ..
 (*<*)
-qed
+end
 (*>*)
 
 text_raw {*\end{minipage}\begin{minipage}{0.4\textwidth}*}
@@ -106,12 +107,13 @@
 *}
 
 (*<*)
-example_proof
+notepad
+begin
 (*>*)
     assume "x \<in> A" and "x \<in> B"
     then have "x \<in> A \<inter> B" by (rule IntI)
 (*<*)
-qed
+end
 (*>*)
 
 text {*
@@ -128,7 +130,8 @@
 text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
 
 (*<*)
-example_proof
+notepad
+begin
 (*>*)
     have "x \<in> \<Inter>\<A>"
     proof
@@ -137,7 +140,7 @@
       show "x \<in> A" sorry %noproof
     qed
 (*<*)
-qed
+end
 (*>*)
 
 text_raw {*\end{minipage}\begin{minipage}{0.4\textwidth}*}
@@ -175,7 +178,8 @@
 text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
 
 (*<*)
-example_proof
+notepad
+begin
 (*>*)
     assume "x \<in> \<Union>\<A>"
     then have C
@@ -185,7 +189,7 @@
       show C sorry %noproof
     qed
 (*<*)
-qed
+end
 (*>*)
 
 text_raw {*\end{minipage}\begin{minipage}{0.4\textwidth}*}
@@ -208,12 +212,13 @@
 *}
 
 (*<*)
-example_proof
+notepad
+begin
 (*>*)
     assume "x \<in> \<Union>\<A>"
     then obtain A where "x \<in> A" and "A \<in> \<A>" ..
 (*<*)
-qed
+end
 (*>*)
 
 text {*
@@ -812,7 +817,7 @@
 *}
 
 text_raw {* \begingroup\footnotesize *}
-(*<*)example_proof
+(*<*)notepad begin
 (*>*)
   txt_raw {* \begin{minipage}[t]{0.18\textwidth} *}
   have "A \<longrightarrow> B"
@@ -853,7 +858,7 @@
 @{text "(finish)"} \\
 \end{minipage} *}
 (*<*)
-qed
+end
 (*>*)
 text_raw {* \endgroup *}
 
@@ -871,7 +876,8 @@
 text_raw {*\begin{minipage}{0.5\textwidth}*}
 
 (*<*)
-example_proof
+notepad
+begin
 (*>*)
   have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"
   proof -
@@ -915,7 +921,7 @@
     show "C x y" sorry
   qed
 (*<*)
-qed
+end
 (*>*)
 
 text_raw {*\end{minipage}*}
@@ -980,14 +986,15 @@
 *}
 
 (*<*)
-example_proof
+notepad
+begin
 (*>*)
   have "a = b" sorry
   also have "\<dots> = c" sorry
   also have "\<dots> = d" sorry
   finally have "a = d" .
 (*<*)
-qed
+end
 (*>*)
 
 text {*