# HG changeset patch
# User wenzelm
# Date 1427925596 -7200
# Node ID 678c9e6257827e4de0be7291e6c459913769e795
# Parent  9d04e2c188b3af0da229de7c65baa52e1b421e55
misc tuning -- keep name space more clean;

diff -r 9d04e2c188b3 -r 678c9e625782 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Wed Apr 01 22:46:49 2015 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Wed Apr 01 23:59:56 2015 +0200
@@ -18,12 +18,14 @@
   this:
 \<close>
 
+(*<*)experiment begin(*>*)
 declare [[show_main_goal = false]]
 
 notepad
 begin
   note [[show_main_goal = true]]
 end
+(*<*)end(*>*)
 
 text \<open>For historical reasons, some tools cannot take the full proof
   context into account and merely refer to the background theory.
@@ -816,7 +818,7 @@
   lexicographically --- the rewriting engine imitates bubble-sort.
 \<close>
 
-locale AC_example =
+experiment
   fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infix "\<bullet>" 60)
   assumes assoc: "(x \<bullet> y) \<bullet> z = x \<bullet> (y \<bullet> z)"
   assumes commute: "x \<bullet> y = y \<bullet> x"
@@ -922,8 +924,10 @@
   \end{description}
 \<close>
 
+(*<*)experiment begin(*>*)
 declare conjI [simp_break]
 declare [[simp_break "?x \<and> ?y"]]
+(*<*)end(*>*)
 
 
 subsection \<open>Simplification procedures \label{sec:simproc}\<close>
@@ -996,10 +1000,12 @@
   the Simplifier loop!  Note that a version of this simplification
   procedure is already active in Isabelle/HOL.\<close>
 
+(*<*)experiment begin(*>*)
 simproc_setup unit ("x::unit") =
   \<open>fn _ => fn _ => fn ct =>
     if HOLogic.is_unit (Thm.term_of ct) then NONE
     else SOME (mk_meta_eq @{thm unit_eq})\<close>
+(*<*)end(*>*)
 
 text \<open>Since the Simplifier applies simplification procedures
   frequently, it is important to make the failure check in ML
@@ -1049,7 +1055,7 @@
   As an example, consider the following alternative subgoaler:
 \<close>
 
-ML \<open>
+ML_val \<open>
   fun subgoaler_tac ctxt =
     assume_tac ctxt ORELSE'
     resolve_tac ctxt (Simplifier.prems_of ctxt) ORELSE'
@@ -1873,7 +1879,7 @@
 
   Initially the two wrapper lists are empty, which means no
   modification of the step tactics. Safe and unsafe wrappers are added
-  to a claset with the functions given below, supplying them with
+  to the context with the functions given below, supplying them with
   wrapper names.  These names may be used to selectively delete
   wrappers.
 
diff -r 9d04e2c188b3 -r 678c9e625782 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Wed Apr 01 22:46:49 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Wed Apr 01 23:59:56 2015 +0200
@@ -220,6 +220,7 @@
 
 text \<open>The finite powerset operator can be defined inductively like this:\<close>
 
+(*<*)experiment begin(*>*)
 inductive_set Fin :: "'a set \<Rightarrow> 'a set set" for A :: "'a set"
 where
   empty: "{} \<in> Fin A"
@@ -230,11 +231,13 @@
 inductive acc :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<prec>" 50)
 where acc: "(\<And>y. y \<prec> x \<Longrightarrow> acc r y) \<Longrightarrow> acc r x"
+(*<*)end(*>*)
 
 text \<open>Common logical connectives can be easily characterized as
 non-recursive inductive definitions with parameters, but without
 arguments.\<close>
 
+(*<*)experiment begin(*>*)
 inductive AND for A B :: bool
 where "A \<Longrightarrow> B \<Longrightarrow> AND A B"
 
@@ -244,6 +247,7 @@
 
 inductive EXISTS for B :: "'a \<Rightarrow> bool"
 where "B a \<Longrightarrow> EXISTS B"
+(*<*)end(*>*)
 
 text \<open>Here the @{text "cases"} or @{text "induct"} rules produced by
   the @{command inductive} package coincide with the expected
@@ -378,6 +382,7 @@
   boolean expressions, and use @{command primrec} for evaluation
   functions that follow the same recursive structure.\<close>
 
+(*<*)experiment begin(*>*)
 datatype 'a aexp =
     IF "'a bexp"  "'a aexp"  "'a aexp"
   | Sum "'a aexp"  "'a aexp"
@@ -442,6 +447,7 @@
   "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a"
   "evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
   by (induct a and b) simp_all
+(*<*)end(*>*)
 
 
 subsubsection \<open>Example: a substitution function for terms\<close>
@@ -449,6 +455,7 @@
 text \<open>Functions on datatypes with nested recursion are also defined
   by mutual primitive recursion.\<close>
 
+(*<*)experiment begin(*>*)
 datatype ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"
 
 text \<open>A substitution function on type @{typ "('a, 'b) term"} can be
@@ -468,9 +475,12 @@
   substitution function, mutual induction is needed:
 \<close>
 
-lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)" and
-  "subst_term_list (subst_term f1 \<circ> f2) ts = subst_term_list f1 (subst_term_list f2 ts)"
+lemma "subst_term (subst_term f1 \<circ> f2) t =
+    subst_term f1 (subst_term f2 t)" and
+  "subst_term_list (subst_term f1 \<circ> f2) ts =
+    subst_term_list f1 (subst_term_list f2 ts)"
   by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all
+(*<*)end(*>*)
 
 
 subsubsection \<open>Example: a map function for infinitely branching trees\<close>
@@ -479,6 +489,7 @@
   primitive recursion is just as easy.
 \<close>
 
+(*<*)experiment begin(*>*)
 datatype 'a tree = Atom 'a | Branch "nat \<Rightarrow> 'a tree"
 
 primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"
@@ -494,6 +505,7 @@
 
 lemma "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
   by (induct t) simp_all
+(*<*)end(*>*)
 
 
 subsection \<open>Proof methods related to recursive definitions\<close>
@@ -748,6 +760,7 @@
   names than the existing @{typ "'a list"} that is already in @{theory
   Main}:\<close>
 
+(*<*)experiment begin(*>*)
 datatype 'a seq = Empty | Seq 'a "'a seq"
 
 text \<open>We can now prove some simple lemma by structural induction:\<close>
@@ -771,6 +784,7 @@
 
 lemma "Seq x xs \<noteq> xs"
   by (induct xs arbitrary: x) simp_all
+(*<*)end(*>*)
 
 
 section \<open>Records \label{sec:hol-record}\<close>
@@ -1118,6 +1132,7 @@
   \end{description}
 \<close>
 
+
 subsubsection \<open>Examples\<close>
 
 text \<open>Type definitions permit the introduction of abstract data
@@ -1142,6 +1157,7 @@
   \medskip The following trivial example pulls a three-element type
   into existence within the formal logical environment of HOL.\<close>
 
+(*<*)experiment begin(*>*)
 typedef three = "{(True, True), (True, False), (False, True)}"
   by blast
 
@@ -1155,11 +1171,14 @@
 lemma three_cases:
   fixes x :: three obtains "x = One" | "x = Two" | "x = Three"
   by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject)
+(*<*)end(*>*)
 
 text \<open>Note that such trivial constructions are better done with
   derived specification mechanisms such as @{command datatype}:\<close>
 
-datatype three' = One' | Two' | Three'
+(*<*)experiment begin(*>*)
+datatype three = One | Two | Three
+(*<*)end(*>*)
 
 text \<open>This avoids re-doing basic definitions and proofs from the
   primitive @{command typedef} above.\<close>
@@ -1988,6 +2007,7 @@
 text \<open>The subsequent example is from geometry: collinearity is
   invariant by rotation.\<close>
 
+(*<*)experiment begin(*>*)
 type_synonym point = "int \<times> int"
 
 fun collinear :: "point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
@@ -1999,6 +2019,7 @@
   shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
     (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
   using assms by (algebra add: collinear.simps)
+(*<*)end(*>*)
 
 text \<open>
  See also @{file "~~/src/HOL/ex/Groebner_Examples.thy"}.
diff -r 9d04e2c188b3 -r 678c9e625782 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Wed Apr 01 22:46:49 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Wed Apr 01 23:59:56 2015 +0200
@@ -952,6 +952,7 @@
   \end{description}
 \<close>
 
+(*<*)experiment begin(*>*)
   method_setup my_method1 =
     \<open>Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))\<close>
     "my first method (without any arguments)"
@@ -965,6 +966,7 @@
     \<open>Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>
       SIMPLE_METHOD' (fn i: int => no_tac))\<close>
     "my third method (with theorem arguments and context)"
+(*<*)end(*>*)
 
 
 section \<open>Generalized elimination \label{sec:obtain}\<close>
diff -r 9d04e2c188b3 -r 678c9e625782 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Wed Apr 01 22:46:49 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Wed Apr 01 23:59:56 2015 +0200
@@ -260,10 +260,12 @@
   Here is an artificial example of bundling various configuration
   options:\<close>
 
+(*<*)experiment begin(*>*)
 bundle trace = [[simp_trace, linarith_trace, metis_trace, smt_trace]]
 
 lemma "x = x"
   including trace by metis
+(*<*)end(*>*)
 
 
 section \<open>Term definitions \label{sec:term-definitions}\<close>
@@ -1205,6 +1207,7 @@
   \end{description}
 \<close>
 
+(*<*)experiment begin(*>*)
   attribute_setup my_rule =
     \<open>Attrib.thms >> (fn ths =>
       Thm.rule_attribute
@@ -1218,6 +1221,7 @@
         (fn th: thm => fn context: Context.generic =>
           let val context' = context
           in context' end))\<close>
+(*<*)end(*>*)
 
 text \<open>
   \begin{description}