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