
diff -r aec7073d4645 -r daf404920ab9 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Tactical.thy	Tue May 14 11:10:53 2019 +0200
@@ -44,8 +44,6 @@
 apply(assumption)
 done
 
-
-
 text {*
   This proof translates to the following ML-code.
   
@@ -55,11 +53,11 @@
   val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
 in
   Goal.prove ctxt [\"P\", \"Q\"] [] goal 
-   (fn _ =>  etac @{thm disjE} 1
-             THEN rtac @{thm disjI2} 1
-             THEN atac 1
-             THEN rtac @{thm disjI1} 1
-             THEN atac 1)
+   (fn _ =>  eresolve_tac @{context} [@{thm disjE}] 1
+             THEN resolve_tac @{context} [@{thm disjI2}] 1
+             THEN assume_tac @{context} 1
+             THEN resolve_tac @{context} [@{thm disjI1}] 1
+             THEN assume_tac @{context} 1)
 end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
   
   To start the proof, the function @{ML_ind prove in Goal} sets up a goal
@@ -70,12 +68,12 @@
   into schematic variables once the goal is proved (in our case @{text P} and
   @{text Q}). The last argument is the tactic that proves the goal. This
   tactic can make use of the local assumptions (there are none in this
-  example). The tactics @{ML_ind etac in Tactic}, @{ML_ind rtac in Tactic} and
-  @{ML_ind atac in Tactic} in the code above correspond roughly to @{text
+  example). The tactics @{ML_ind eresolve_tac in Tactic}, @{ML_ind resolve_tac in Tactic} and
+  @{ML_ind assume_tac in Tactic} in the code above correspond roughly to @{text
   erule}, @{text rule} and @{text assumption}, respectively. The combinator
   @{ML THEN} strings the tactics together.
 
-  TBD: Write something about @{ML_ind prove_multi in Goal}.
+  TBD: Write something about @{ML_ind prove_common in Goal}.
 
   \begin{readmore}
   To learn more about the function @{ML_ind prove in Goal} see
@@ -96,18 +94,18 @@
 
 *}
 
-ML %grayML{*val foo_tac = 
-      (etac @{thm disjE} 1
-       THEN rtac @{thm disjI2} 1
-       THEN atac 1
-       THEN rtac @{thm disjI1} 1
-       THEN atac 1)*}
+ML %grayML{*fun foo_tac ctxt = 
+      (eresolve_tac ctxt [@{thm disjE}] 1
+       THEN resolve_tac  ctxt [@{thm disjI2}] 1
+       THEN assume_tac  ctxt 1
+       THEN resolve_tac ctxt [@{thm disjI1}] 1
+       THEN assume_tac  ctxt 1)*}
 
 text {* and the Isabelle proof: *}
 
 lemma 
   shows "P \<or> Q \<Longrightarrow> Q \<or> P"
-apply(tactic {* foo_tac *})
+apply(tactic {* foo_tac @{context} *})
 done
 
 text {*
@@ -125,12 +123,12 @@
   you can write
 *}
 
-ML %grayML{*val foo_tac' = 
-      (etac @{thm disjE} 
-       THEN' rtac @{thm disjI2} 
-       THEN' atac 
-       THEN' rtac @{thm disjI1} 
-       THEN' atac)*}text_raw{*\label{tac:footacprime}*}
+ML %grayML{*fun foo_tac' ctxt = 
+      (eresolve_tac ctxt [@{thm disjE}] 
+       THEN' resolve_tac ctxt [@{thm disjI2}] 
+       THEN' assume_tac ctxt 
+       THEN' resolve_tac ctxt [@{thm disjI1}] 
+       THEN' assume_tac ctxt)*}text_raw{*\label{tac:footacprime}*}
 
 text {* 
   where @{ML_ind THEN' in Tactical} is used instead of @{ML THEN in
@@ -144,8 +142,8 @@
 lemma 
   shows "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"
   and   "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2"
-apply(tactic {* foo_tac' 2 *})
-apply(tactic {* foo_tac' 1 *})
+apply(tactic {* foo_tac' @{context} 2 *})
+apply(tactic {* foo_tac' @{context} 1 *})
 done
 
 text {*
@@ -203,7 +201,7 @@
 
 lemma 
   shows "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
-apply(tactic {* foo_tac' 1 *})
+apply(tactic {* foo_tac' @{context} 1 *})
 back
 done
 
@@ -350,7 +348,7 @@
 where
   "EQ_TRUE X \<equiv> (X = True)"
 
-schematic_lemma test: 
+schematic_goal test: 
   shows "EQ_TRUE ?X"
 unfolding EQ_TRUE_def
 by (rule refl)
@@ -407,28 +405,28 @@
 
 lemma 
   shows "False" and "Goldbach_conjecture"  
-apply(tactic {* Skip_Proof.cheat_tac 1 *})
+apply(tactic {* Skip_Proof.cheat_tac @{context} 1 *})
 txt{*\begin{minipage}{\textwidth}
      @{subgoals [display]}
      \end{minipage}*}
 (*<*)oops(*>*)
 
 text {*
-  Another simple tactic is the function @{ML_ind atac in Tactic}, which, as shown 
+  Another simple tactic is the function @{ML_ind assume_tac in Tactic}, which, as shown 
   earlier, corresponds to the assumption method.
 *}
 
 lemma 
   shows "P \<Longrightarrow> P"
-apply(tactic {* atac 1 *})
+apply(tactic {* assume_tac @{context} 1 *})
 txt{*\begin{minipage}{\textwidth}
      @{subgoals [display]}
      \end{minipage}*}
 (*<*)oops(*>*)
 
 text {*
-  Similarly, @{ML_ind rtac in Tactic}, @{ML_ind dtac in Tactic}, @{ML_ind etac
-  in Tactic} and @{ML_ind ftac in Tactic} correspond (roughly) to @{text
+  Similarly, @{ML_ind resolve_tac in Tactic}, @{ML_ind dresolve_tac in Tactic}, @{ML_ind eresolve_tac
+  in Tactic} and @{ML_ind forward_tac in Tactic} correspond (roughly) to @{text
   rule}, @{text drule}, @{text erule} and @{text frule}, respectively. Each of
   them takes a theorem as argument and attempts to apply it to a goal. Below
   are three self-explanatory examples.
@@ -436,7 +434,7 @@
 
 lemma 
   shows "P \<and> Q"
-apply(tactic {* rtac @{thm conjI} 1 *})
+apply(tactic {* resolve_tac @{context} [@{thm conjI}] 1 *})
 txt{*\begin{minipage}{\textwidth}
      @{subgoals [display]}
      \end{minipage}*}
@@ -444,7 +442,7 @@
 
 lemma 
   shows "P \<and> Q \<Longrightarrow> False"
-apply(tactic {* etac @{thm conjE} 1 *})
+apply(tactic {* eresolve_tac @{context} [@{thm conjE}] 1 *})
 txt{*\begin{minipage}{\textwidth}
      @{subgoals [display]}
      \end{minipage}*}
@@ -452,20 +450,20 @@
 
 lemma 
   shows "False \<and> True \<Longrightarrow> False"
-apply(tactic {* dtac @{thm conjunct2} 1 *})
+apply(tactic {* dresolve_tac @{context} [@{thm conjunct2}] 1 *})
 txt{*\begin{minipage}{\textwidth}
      @{subgoals [display]}
      \end{minipage}*}
 (*<*)oops(*>*)
 
 text {*
-  The function @{ML_ind resolve_tac in Tactic} is similar to @{ML rtac}, except that it
+  The function @{ML_ind resolve_tac in Tactic} 
   expects a list of theorems as argument. From this list it will apply the
   first applicable theorem (later theorems that are also applicable can be
   explored via the lazy sequences mechanism). Given the code
 *}
 
-ML %grayML{*val resolve_xmp_tac = resolve_tac [@{thm impI}, @{thm conjI}]*}
+ML %grayML{*fun resolve_xmp_tac ctxt = resolve_tac ctxt [@{thm impI}, @{thm conjI}]*}
 
 text {*
   an example for @{ML resolve_tac} is the following proof where first an outermost 
@@ -475,8 +473,8 @@
 lemma 
   shows "C \<longrightarrow> (A \<and> B)" 
   and   "(A \<longrightarrow> B) \<and> C"
-apply(tactic {* resolve_xmp_tac 1 *})
-apply(tactic {* resolve_xmp_tac 2 *})
+apply(tactic {* resolve_xmp_tac @{context} 1 *})
+apply(tactic {* resolve_xmp_tac @{context} 2 *})
 txt{*\begin{minipage}{\textwidth}
      @{subgoals [display]} 
      \end{minipage}*}
@@ -484,8 +482,8 @@
 
 text {* 
   Similar versions taking a list of theorems exist for the tactics 
-  @{ML dtac} (@{ML_ind dresolve_tac in Tactic}), @{ML etac} 
-  (@{ML_ind eresolve_tac in Tactic}) and so on.
+   @{ML_ind dresolve_tac in Tactic},  
+  @{ML_ind eresolve_tac in Tactic} and so on.
 
   Another simple tactic is @{ML_ind cut_facts_tac in Tactic}. It inserts a
   list of theorems into the assumptions of the current goal state. Below we
@@ -521,7 +519,7 @@
 \begin{isabelle}
 *}
 
-ML %grayML{*fun foc_tac {prems, params, asms, concl, context, schematics} = 
+ML %grayML{*fun foc_tac {context, params, prems, asms, concl, schematics} = 
 let 
   fun assgn1 f1 f2 xs =
     let
@@ -530,7 +528,7 @@
       Pretty.list "" "" out
     end 
 
-  fun assgn2 f xs = assgn1 f f xs 
+  fun assgn2 f xs = assgn1 (fn (n,T) => pretty_term context (Var (n,T))) f  xs 
  
   val pps = map (fn (s, pp) => Pretty.block [Pretty.str s, pp])
     [("params: ", assgn1 Pretty.str (pretty_cterm context) params),
@@ -552,7 +550,7 @@
 \end{figure}
 *}
 
-schematic_lemma 
+schematic_goal
   shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
 apply(tactic {* Subgoal.FOCUS foc_tac @{context} 1 *})
 
@@ -608,15 +606,15 @@
   variables.
 
   Observe that inside @{ML FOCUS in Subgoal} and @{ML SUBPROOF}, we are in a goal
-  state where there is only a conclusion. This means the tactics @{ML dtac} and 
+  state where there is only a conclusion. This means the tactics @{ML dresolve_tac} and 
   the like are of no use for manipulating the goal state. The assumptions inside 
   @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are given as cterms and theorems in 
   the arguments @{text "asms"} and @{text "prems"}, respectively. This 
   means we can apply them using the usual assumption tactics. With this you can 
-  for example easily implement a tactic that behaves almost like @{ML atac}:
+  for example easily implement a tactic that behaves almost like @{ML assume_tac}:
 *}
 
-ML %grayML{*val atac' = Subgoal.FOCUS (fn {prems, ...} => resolve_tac prems 1)*}
+ML %grayML{*val atac' = Subgoal.FOCUS (fn {prems, context, ...} => resolve_tac context prems 1)*}
 
 text {*
   If you apply @{ML atac'} to the next lemma
@@ -656,7 +654,7 @@
 
   \begin{readmore}
   The functions @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are defined in 
-  @{ML_file "Pure/subgoal.ML"} and also described in 
+  @{ML_file "Pure/Isar/subgoal.ML"} and also described in 
   \isccite{sec:results}. 
   \end{readmore}
 
@@ -669,14 +667,14 @@
   analyse a few connectives). The code of the tactic is as follows.
 *}
 
-ML %linenosgray{*fun select_tac (t, i) =
+ML %linenosgray{*fun select_tac ctxt (t, i) =
   case t of
-     @{term "Trueprop"} $ t' => select_tac (t', i)
-   | @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t', i)
-   | @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i
-   | @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i
-   | @{term "Not"} $ _ => rtac @{thm notI} i
-   | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i
+     @{term "Trueprop"} $ t' => select_tac ctxt (t', i)
+   | @{term "(\<Longrightarrow>)"} $ _ $ t' => select_tac ctxt (t', i)
+   | @{term "(\<and>)"} $ _ $ _ => resolve_tac ctxt [@{thm conjI}] i
+   | @{term "(\<longrightarrow>)"} $ _ $ _ => resolve_tac ctxt [@{thm impI}] i
+   | @{term "Not"} $ _ => resolve_tac ctxt [@{thm notI}] i
+   | Const (@{const_name "All"}, _) $ _ => resolve_tac ctxt [@{thm allI}] i
    | _ => all_tac*}text_raw{*\label{tac:selecttac}*}
 
 text {*
@@ -702,10 +700,10 @@
 
 lemma 
   shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
-apply(tactic {* SUBGOAL select_tac 4 *})
-apply(tactic {* SUBGOAL select_tac 3 *})
-apply(tactic {* SUBGOAL select_tac 2 *})
-apply(tactic {* SUBGOAL select_tac 1 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 4 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 3 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 2 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 1 *})
 txt{* \begin{minipage}{\textwidth}
       @{subgoals [display]}
       \end{minipage} *}
@@ -720,10 +718,10 @@
 
 lemma 
   shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
-apply(tactic {* SUBGOAL select_tac 1 *})
-apply(tactic {* SUBGOAL select_tac 3 *})
-apply(tactic {* SUBGOAL select_tac 4 *})
-apply(tactic {* SUBGOAL select_tac 5 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 1 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 3 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 4 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 5 *})
 (*<*)oops(*>*)
 
 text {*
@@ -743,7 +741,7 @@
   \end{readmore}
 
 
-  Since @{ML_ind rtac in Tactic} and the like use higher-order unification, an
+  Since @{ML_ind resolve_tac in Tactic} and the like use higher-order unification, an
   automatic proof procedure based on them might become too fragile, if it just
   applies theorems as shown above. The reason is that a number of theorems
   introduce schematic variables into the goal state. Consider for example the
@@ -752,7 +750,7 @@
 
 lemma 
   shows "\<forall>x \<in> A. P x \<Longrightarrow> Q x"
-apply(tactic {* dtac @{thm bspec} 1 *})
+apply(tactic {* dresolve_tac @{context} [@{thm bspec}] 1 *})
 txt{*\begin{minipage}{\textwidth}
      @{subgoals [display]} 
      \end{minipage}*}
@@ -849,7 +847,7 @@
 lemma 
   fixes x y u w::"'a"
   shows "t x y = s u w"
-apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+apply(tactic {* Cong_Tac.cong_tac @{context} @{thm cong} 1 *})
 txt{*\begin{minipage}{\textwidth}
      @{subgoals [display]}
      \end{minipage}*}
@@ -881,12 +879,12 @@
   this we implement the following function.
 *}
 
-ML %linenosgray{*fun fo_rtac thm = Subgoal.FOCUS (fn {concl, ...} =>
+ML %linenosgray{*fun fo_rtac thm = Subgoal.FOCUS (fn {context, concl, ...} =>
   let 
-    val concl_pat = Drule.strip_imp_concl (cprop_of thm)
+    val concl_pat = Drule.strip_imp_concl (Thm.cprop_of thm)
     val insts = Thm.first_order_match (concl_pat, concl)
   in
-    rtac (Drule.instantiate_normalize insts thm) 1
+    resolve_tac context [(Drule.instantiate_normalize insts thm)] 1
   end)*}
 
 text {*
@@ -930,7 +928,7 @@
 
 lemma 
   shows "(Foo \<and> Bar) \<and> False"
-apply(tactic {* rtac @{thm conjI} 1 THEN rtac @{thm conjI} 1 *})
+apply(tactic {* resolve_tac @{context} [@{thm conjI}] 1 THEN resolve_tac @{context} [@{thm conjI}] 1 *})
 txt {* \begin{minipage}{\textwidth}
        @{subgoals [display]} 
        \end{minipage} *}
@@ -944,7 +942,7 @@
 
 lemma 
   shows "(Foo \<and> Bar) \<and> False"
-apply(tactic {* (rtac @{thm conjI} THEN' rtac @{thm conjI}) 1 *})
+apply(tactic {* (resolve_tac @{context} [@{thm conjI}] THEN' resolve_tac @{context} [@{thm conjI}]) 1 *})
 txt {* \begin{minipage}{\textwidth}
        @{subgoals [display]} 
        \end{minipage} *}
@@ -964,8 +962,8 @@
 
 lemma 
   shows "A \<Longrightarrow> True \<and> A"
-apply(tactic {* (rtac @{thm conjI} 
-                 THEN' RANGE [rtac @{thm TrueI}, atac]) 1 *})
+apply(tactic {* (resolve_tac @{context} [@{thm conjI}] 
+                 THEN' RANGE [resolve_tac @{context} [@{thm TrueI}], assume_tac @{context}]) 1 *})
 txt {* \begin{minipage}{\textwidth}
        @{subgoals [display]} 
        \end{minipage} *}
@@ -978,19 +976,21 @@
   page~\pageref{tac:footacprime} can also be written as:
 *}
 
-ML %grayML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2}, 
-                        atac, rtac @{thm disjI1}, atac]*}
+ML %grayML{*fun foo_tac'' ctxt = 
+  EVERY' [eresolve_tac ctxt [@{thm disjE}], resolve_tac ctxt [@{thm disjI2}], 
+          assume_tac ctxt, resolve_tac ctxt [@{thm disjI1}], assume_tac ctxt]*}
 
 text {*
   There is even another way of implementing this tactic: in automatic proof
   procedures (in contrast to tactics that might be called by the user) there
   are often long lists of tactics that are applied to the first
-  subgoal. Instead of writing the code above and then calling @{ML "foo_tac'' 1"}, 
+  subgoal. Instead of writing the code above and then calling @{ML "foo_tac'' @{context} 1"}, 
   you can also just write
 *}
 
-ML %grayML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2}, 
-                       atac, rtac @{thm disjI1}, atac]*}
+ML %grayML{*fun foo_tac1 ctxt = 
+  EVERY1 [eresolve_tac ctxt [@{thm disjE}], resolve_tac ctxt [@{thm disjI2}], 
+          assume_tac ctxt, resolve_tac ctxt [@{thm disjI1}], assume_tac ctxt]*}
 
 text {*
   and call @{ML foo_tac1}.  
@@ -1003,7 +1003,8 @@
 
 *}
 
-ML %grayML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
+ML %grayML{*fun orelse_xmp_tac ctxt = 
+  resolve_tac ctxt [@{thm disjI1}] ORELSE' resolve_tac ctxt [@{thm conjI}]*}
 
 text {*
   will first try out whether theorem @{text disjI} applies and in case of failure 
@@ -1012,8 +1013,8 @@
 
 lemma 
   shows "True \<and> False" and "Foo \<or> Bar"
-apply(tactic {* orelse_xmp_tac 2 *})
-apply(tactic {* orelse_xmp_tac 1 *})
+apply(tactic {* orelse_xmp_tac @{context} 2 *})
+apply(tactic {* orelse_xmp_tac @{context} 1 *})
 txt {* which results in the goal state
        \begin{isabelle}
        @{subgoals [display]} 
@@ -1027,8 +1028,9 @@
   as follows:
 *}
 
-ML %grayML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI}, 
-                          rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}text_raw{*\label{tac:selectprime}*}
+ML %grayML{*fun select_tac' ctxt = 
+  FIRST' [resolve_tac ctxt [@{thm conjI}], resolve_tac ctxt [@{thm impI}], 
+          resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{thm allI}], K all_tac]*}text_raw{*\label{tac:selectprime}*}
 
 text {*
   Since we like to mimic the behaviour of @{ML select_tac} as closely as possible, 
@@ -1040,10 +1042,10 @@
 
 lemma 
   shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
-apply(tactic {* select_tac' 4 *})
-apply(tactic {* select_tac' 3 *})
-apply(tactic {* select_tac' 2 *})
-apply(tactic {* select_tac' 1 *})
+apply(tactic {* select_tac' @{context} 4 *})
+apply(tactic {* select_tac' @{context} 3 *})
+apply(tactic {* select_tac' @{context} 2 *})
+apply(tactic {* select_tac' @{context} 1 *})
 txt{* \begin{minipage}{\textwidth}
       @{subgoals [display]}
       \end{minipage} *}
@@ -1057,7 +1059,7 @@
 
 lemma 
   shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
-apply(tactic {* ALLGOALS select_tac' *})
+apply(tactic {* ALLGOALS (select_tac' @{context}) *})
 txt{* \begin{minipage}{\textwidth}
       @{subgoals [display]}
       \end{minipage} *}
@@ -1070,8 +1072,9 @@
   For example:
 *}
 
-ML %grayML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI}, 
-                                 rtac @{thm notI}, rtac @{thm allI}]*}
+ML %grayML{*fun select_tac'' ctxt = 
+ TRY o FIRST' [resolve_tac ctxt [@{thm conjI}], resolve_tac ctxt [@{thm impI}], 
+               resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{thm allI}]]*}
 text_raw{*\label{tac:selectprimeprime}*}
 
 text {*
@@ -1084,7 +1087,7 @@
 
 lemma 
   shows "E \<Longrightarrow> F"
-apply(tactic {* select_tac' 1 *})
+apply(tactic {* select_tac' @{context} 1 *})
 txt{* \begin{minipage}{\textwidth}
       @{subgoals [display]}
       \end{minipage} *}
@@ -1107,7 +1110,7 @@
 
 lemma 
   shows "E \<Longrightarrow> F"
-apply(tactic {* CHANGED (select_tac' 1) *})(*<*)?(*>*)
+apply(tactic {* CHANGED (select_tac' @{context} 1) *})(*<*)?(*>*)
 txt{* gives the error message:
   \begin{isabelle}
   @{text "*** empty result sequence -- proof command failed"}\\
@@ -1123,13 +1126,13 @@
   suppose the following tactic
 *}
 
-ML %grayML{*val repeat_xmp_tac = REPEAT (CHANGED (select_tac' 1)) *}
+ML %grayML{*fun repeat_xmp_tac ctxt = REPEAT (CHANGED (select_tac' ctxt 1)) *}
 
 text {* which applied to the proof *}
 
 lemma 
   shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
-apply(tactic {* repeat_xmp_tac *})
+apply(tactic {* repeat_xmp_tac @{context} *})
 txt{* produces
       \begin{isabelle}
       @{subgoals [display]}
@@ -1147,7 +1150,7 @@
   can implement it as
 *}
 
-ML %grayML{*val repeat_xmp_tac' = REPEAT o CHANGED o select_tac'*}
+ML %grayML{*fun repeat_xmp_tac' ctxt = REPEAT o CHANGED o select_tac' ctxt*}
 
 text {*
   since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}.
@@ -1160,7 +1163,7 @@
   Supposing the tactic
 *}
 
-ML %grayML{*val repeat_all_new_xmp_tac = REPEAT_ALL_NEW (CHANGED o select_tac')*}
+ML %grayML{*fun repeat_all_new_xmp_tac ctxt = REPEAT_ALL_NEW (CHANGED o select_tac' ctxt)*}
 
 text {* 
   you can see that the following goal
@@ -1168,7 +1171,7 @@
 
 lemma 
   shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
-apply(tactic {* repeat_all_new_xmp_tac 1 *})
+apply(tactic {* repeat_all_new_xmp_tac @{context} 1 *})
 txt{* \begin{minipage}{\textwidth}
       @{subgoals [display]}
       \end{minipage} *}
@@ -1185,7 +1188,7 @@
 
 lemma 
   shows "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
-apply(tactic {* etac @{thm disjE} 1 *})
+apply(tactic {* eresolve_tac @{context} [@{thm disjE}] 1 *})
 txt{* applies the rule to the first assumption yielding the goal state:
       \begin{isabelle}
       @{subgoals [display]}
@@ -1197,7 +1200,7 @@
 oops
 lemma 
   shows "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
-apply(tactic {* etac @{thm disjE} 1 *})
+apply(tactic {* eresolve_tac @{context} [@{thm disjE}] 1 *})
 (*>*)
 back
 txt{* the rule now applies to the second assumption.
@@ -1215,7 +1218,7 @@
 
 lemma 
   shows "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
-apply(tactic {* DETERM (etac @{thm disjE} 1) *})
+apply(tactic {* DETERM (eresolve_tac @{context} [@{thm disjE}] 1) *})
 txt {*\begin{minipage}{\textwidth}
       @{subgoals [display]}
       \end{minipage} *}
@@ -1434,12 +1437,12 @@
     Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]
   fun name_cthm ((_, nm), thm) =
     Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]
-  fun name_ctrm (nm, ctrm) =
-    Pretty.enclose (nm ^ ": ") "" [pretty_cterms ctxt ctrm]
+  fun name_trm (nm, trm) =
+    Pretty.enclose (nm ^ ": ") "" [pretty_terms ctxt trm]
 
   val pps = [Pretty.big_list "Simplification rules:" (map name_sthm simps),
              Pretty.big_list "Congruences rules:" (map name_cthm congs),
-             Pretty.big_list "Simproc patterns:" (map name_ctrm procs)]
+             Pretty.big_list "Simproc patterns:" (map name_trm procs)]
 in
   pps |> Pretty.chunks
       |> pwriteln
@@ -1748,7 +1751,7 @@
   often be done easier by implementing a simproc or a conversion. Both will be 
   explained in the next two chapters.
 
-  (FIXME: Is it interesting to say something about @{term "op =simp=>"}?)
+  (FIXME: Is it interesting to say something about @{term "(=simp=>)"}?)
 
   (FIXME: What are the second components of the congruence rules---something to
   do with weak congruence constants?)
@@ -1846,10 +1849,10 @@
   to
 *}
 
-ML %grayML{*fun fail_simproc' ctxt redex = 
+ML %grayML{*fun fail_simproc' _ ctxt redex = 
 let
   val _ = pwriteln (Pretty.block 
-    [Pretty.str "The redex:", pretty_term ctxt redex])
+    [Pretty.str "The redex:", pretty_cterm ctxt redex])
 in
   NONE
 end*}
@@ -1858,17 +1861,12 @@
   Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm}
   (therefore we printing it out using the function @{ML pretty_term in Pretty}).
   We can turn this function into a proper simproc using the function 
-  @{ML Simplifier.simproc_global_i}:
+  @{ML Simplifier.make_simproc}:
 *}
 
-
-ML %grayML{*fun fail' ctxt = 
-let 
-  val thy = @{theory}
-  val pat = [@{term "Suc n"}]
-in
-  Simplifier.simproc_global_i thy "fail_simproc'" pat (K fail_simproc' ctxt)
-end*}
+ML %grayML{*val fail' = 
+  Simplifier.make_simproc @{context} "fail_simproc'"
+    {lhss = [@{term "Suc n"}], proc = fail_simproc'}*}
 
 text {*
   Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
@@ -1883,7 +1881,7 @@
 
 lemma 
   shows "Suc (Suc 0) = (Suc 1)"
-apply(tactic {* simp_tac ((put_simpset HOL_basic_ss @{context}) addsimprocs [fail' @{context}]) 1*})
+apply(tactic {* simp_tac ((put_simpset HOL_basic_ss @{context}) addsimprocs [fail']) 1*})
 (*<*)oops(*>*)
 
 text {*
@@ -1910,8 +1908,8 @@
 *}
 
 
-ML %grayML{*fun plus_one_simproc ctxt redex =
-  case redex of
+ML %grayML{*fun plus_one_simproc _ ctxt redex =
+  case Thm.term_of redex of
     @{term "Suc 0"} => NONE
   | _ => SOME @{thm plus_one}*}
 
@@ -1919,13 +1917,9 @@
   and set up the simproc as follows.
 *}
 
-ML %grayML{*fun plus_one ctxt =
-let
-  val thy = @{theory}
-  val pat = [@{term "Suc n"}] 
-in
-  Simplifier.simproc_global_i thy "sproc +1" pat (K plus_one_simproc ctxt)
-end*}
+ML %grayML{*val plus_one =
+  Simplifier.make_simproc @{context} "sproc +1"
+    {lhss = [@{term "Suc n"}], proc = plus_one_simproc}*}
 
 text {*
   Now the simproc is set up so that it is triggered by terms
@@ -1936,7 +1930,7 @@
 
 lemma 
   shows "P (Suc (Suc (Suc 0))) (Suc 0)"
-apply(tactic {* simp_tac (put_simpset HOL_basic_ss @{context} addsimprocs [plus_one @{context}]) 1*})
+apply(tactic {* simp_tac (put_simpset HOL_basic_ss @{context} addsimprocs [plus_one]) 1*})
 txt{*
   where the simproc produces the goal state
   \begin{isabelle}
@@ -2011,8 +2005,8 @@
   theorem for the simproc.
 *}
 
-ML %grayML{*fun nat_number_simproc ctxt t =
-  SOME (get_thm_alt ctxt (t, dest_suc_trm t))
+ML %grayML{*fun nat_number_simproc _ ctxt ct =
+  SOME (get_thm_alt ctxt (Thm.term_of ct, dest_suc_trm (Thm.term_of ct)))
   handle TERM _ => NONE *}
 
 text {*
@@ -2022,13 +2016,10 @@
   on an example, you can set it up as follows:
 *}
 
-ML %grayML{*fun nat_number ctxt =
-let
-  val thy = @{theory}
-  val pat = [@{term "Suc n"}]
-in 
-  Simplifier.simproc_global_i thy "nat_number" pat (K nat_number_simproc ctxt) 
-end*}
+ML %grayML{*val nat_number =
+  Simplifier.make_simproc @{context} "nat_number"
+    {lhss = [@{term "Suc n"}], proc = nat_number_simproc}*}
+
 
 text {* 
   Now in the lemma
@@ -2036,7 +2027,7 @@
 
 lemma 
   shows "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
-apply(tactic {* simp_tac (put_simpset HOL_ss @{context} addsimprocs [nat_number @{context}]) 1*})
+apply(tactic {* simp_tac (put_simpset HOL_ss @{context} addsimprocs [nat_number]) 1*})
 txt {* 
   you obtain the more legible goal state
   \begin{isabelle}
@@ -2276,7 +2267,7 @@
 
 ML %linenosgray{*fun true_conj1_conv ctxt ctrm =
   case (Thm.term_of ctrm) of
-    @{term "op \<and>"} $ @{term True} $ _ => 
+    @{term "(\<and>)"} $ @{term True} $ _ => 
       (Conv.arg_conv (true_conj1_conv ctxt) then_conv
          Conv.rewr_conv @{thm true_conj1}) ctrm
   | _ $ _ => Conv.comb_conv (true_conj1_conv ctxt) ctrm
@@ -2491,12 +2482,11 @@
 
 ML %linenosgray{*fun unabs_def ctxt def =
 let
-  val (lhs, rhs) = Thm.dest_equals (cprop_of def)
-  val xs = strip_abs_vars (term_of rhs)
+  val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of def)
+  val xs = strip_abs_vars (Thm.term_of rhs)
   val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
   
-  val thy = Proof_Context.theory_of ctxt'
-  val cxs = map (cterm_of thy o Free) xs
+  val cxs = map (Thm.cterm_of ctxt' o Free) xs
   val new_lhs = Drule.list_comb (lhs, cxs)
 
   fun get_conv [] = Conv.rewr_conv def




