--- a/ProgTutorial/Tactical.thy	Sat Aug 28 13:37:25 2010 +0800
+++ b/ProgTutorial/Tactical.thy	Fri Oct 29 11:00:37 2010 +0100
@@ -39,6 +39,8 @@
 apply(assumption)
 done
 
+
+
 text {*
   This proof translates to the following ML-code.
   
@@ -79,34 +81,6 @@
   Manual.
   \end{readmore}
 
-  Note that in the code above we use antiquotations for referencing the
-  theorems. We  could also just have written @{ML "etac disjE 1"} because 
-  many of the basic theorems have a corresponding ML-binding:
-
-  @{ML_response_fake [gray,display]
-  "disjE"
-  "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}
-
-  In case where no ML-binding exists, theorems can also be looked up dynamically 
-  using the function @{ML thm} and the (string) name of the theorem. For example: 
-
-  @{ML_response_fake [gray,display]
-  "thm \"disjE\""
-  "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}
-
-  Both ways however are considered \emph{bad} style! The reason is that the binding
-  for @{ML disjE} can be re-assigned and thus one does not have
-  complete control over which theorem is actually applied. Similarly with the
-  lookup of @{text [quotes] "disjE"}. Although theorems must have a unique name
-  in the theorem database, the string can stand for a dynamically updatable
-  theorem list. Also in this case we cannot be sure which theorem is applied.
-  These problems can be nicely prevented by using antiquotations
-
-  @{ML_response_fake [gray,display]
-  "@{thm \"disjE\"}"
-  "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}
-
-  because then the theorems are fixed statically at compile-time.
 
   \index{tactic@ {\tt\slshape{}tactic}}
   \index{raw\_tactic@ {\tt\slshape{}raw\_tactic}}
@@ -664,39 +638,8 @@
 apply(rule TrueI)
 done
 
-
 text {*
-  There is one peculiarity about @{ML FOCUS in Subgoal} and @{ML SUBPROOF}.
-  If we apply @{text "rtac @{thm allI}"} in the proof below
-*}
-
-lemma
-  shows "B \<Longrightarrow> \<forall>x. A x"
-apply(tactic {* rtac @{thm allI} 1 *})
-txt{* it will produce the expected goal state
-      @{subgoals [display]} *}
-(*<*)oops(*>*)
-
-text {* But if we apply the same tactic inside @{ML FOCUS in Subgoal}
-  we obtain
-*}
-
-lemma
-  shows "B \<Longrightarrow> \<forall>x. A x"
-apply(tactic {* Subgoal.FOCUS (fn _ => rtac @{thm allI} 1) @{context} 1 *})
-txt{* it will produce the goal state
-      @{subgoals [display]} 
-
-  If we want to imitate the behaviour of the ``plain'' tactic, then we
-  can apply the tactic @{ML norm_hhf_tac in Goal}. This gives
-*}
-apply(tactic {* Goal.norm_hhf_tac 1 *})
-txt{*@{subgoals [display]}*}
-(*<*)oops(*>*)
-
-text {*
-  This tactic transforms the goal state into a \emph{hereditary Harrop normal
-  form}. To sum up, both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are rather
+  To sum up, both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are rather
   convenient, but can impose a considerable run-time penalty in automatic
   proofs. If speed is of the essence, then maybe the two lower level combinators 
   described next are more appropriate.