src/Doc/Implementation/Prelim.thy

   show_types} controls output of explicit type constraints for
   variables in printed terms (cf.\ \secref{sec:read-print}).  Its
   value can be modified within Isar text like this:
 \<close>
 
+experiment
+begin
+
 declare [[show_types = false]]
   -- \<open>declaration within (local) theory context\<close>
 
 notepad
 begin

 
   have "x = x"
     using [[show_types = false]]
       -- \<open>declaration within proof (backward mode)\<close>
     ..
+end
+
 end
 
 text \<open>Configuration options that are not set explicitly hold a
   default value that can depend on the application context.  This
   allows to retrieve the value from another slot within the context,

 \<close>
 
 text %mlex \<open>The following simple examples demonstrate how to produce
   fresh names from the initial @{ML Name.context}.\<close>
 
-ML \<open>
+ML_val \<open>
   val list1 = Name.invent Name.context "a" 5;
   @{assert} (list1 = ["a", "b", "c", "d", "e"]);
 
   val list2 =
     #1 (fold_map Name.variant ["x", "x", "a", "a", "'a", "'a"] Name.context);

 \<close>
 
 text \<open>\medskip The same works relatively to the formal context as
   follows.\<close>
 
-locale ex = fixes a b c :: 'a
+experiment fixes a b c :: 'a
 begin
 
-ML \<open>
+ML_val \<open>
   val names = Variable.names_of @{context};
 
   val list1 = Name.invent names "a" 5;
   @{assert} (list1 = ["d", "e", "f", "g", "h"]);
 

 
 text %mlex \<open>The following example yields the source position of some
   concrete binding inlined into the text:
 \<close>
 
-ML \<open>Binding.pos_of @{binding here}\<close>
+ML_val \<open>Binding.pos_of @{binding here}\<close>
 
 text \<open>\medskip That position can be also printed in a message as
   follows:\<close>
 
 ML_command