--- a/CookBook/Tactical.thy	Wed Mar 04 13:15:29 2009 +0000
+++ b/CookBook/Tactical.thy	Wed Mar 04 13:50:47 2009 +0000
@@ -1,6 +1,5 @@
 theory Tactical
 imports Base FirstSteps
-uses "infix_conv.ML"
 begin
 
 chapter {* Tactical Reasoning\label{chp:tactical} *}
@@ -479,21 +478,10 @@
   takes an additional number as argument that makes explicit which premise 
   should be instantiated. 
 
-  To improve readability of the theorems we produce below, we shall use 
-  the following function
-*}
-
-ML{*fun no_vars ctxt thm =
-let 
-  val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt
-in
-  thm'
-end*}
-
-text {*
-  that transform the schematic variables of a theorem into free variables.
-  Using this function for the first @{ML RS}-expression above would produce
-  the more readable result:
+  To improve readability of the theorems we produce below, we shall use the
+  function @{ML no_vars} from Section~\ref{sec:printing}, which transforms
+  schematic variables into free ones.  Using this function for the first @{ML
+  RS}-expression above produces the more readable result:
 
   @{ML_response_fake [display,gray]
   "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}
@@ -1018,7 +1006,7 @@
 
 *}
 
-section {* Simplifier Tactics (TBD) *}
+section {* Simplifier Tactics *}
 
 text {*
   A lot of convenience in the reasoning with Isabelle derives from its
@@ -1188,9 +1176,11 @@
   @{ML_response_fake [display,gray]
   "print_parts @{context} ss1"
 "Simplification rules:
-  ??.unknown: ?A1 - ?B1 \<inter> ?C1 \<equiv> ?A1 - ?B1 \<union> (?A1 - ?C1)
+  ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:"}
 
+  (FIXME: Why does it print out ??.unknown)
+
   Adding the congruence rule @{thm [source] UN_cong} 
 *}
 
@@ -1202,10 +1192,9 @@
   @{ML_response_fake [display,gray]
   "print_parts @{context} ss2"
 "Simplification rules:
-  ??.unknown: ?A1 - ?B1 \<inter> ?C1 \<equiv> ?A1 - ?B1 \<union> (?A1 - ?C1)
+  ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:
-  UNION: \<lbrakk>?A1 = ?B1; \<And>x. x \<in> ?B1 \<Longrightarrow> ?C1 x = ?D1 x\<rbrakk> \<Longrightarrow> 
-     \<Union>x\<in>?A1. ?C1 x \<equiv> \<Union>x\<in>?B1. ?D1 x"}
+  UNION: \<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk> \<Longrightarrow> \<Union>x\<in>A. C x \<equiv> \<Union>x\<in>B. D x"}
 
   Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} 
   expects this form of the simplification and congruence rules. However, even 
@@ -1240,14 +1229,14 @@
   @{ML_response_fake [display,gray]
   "print_parts @{context} HOL_ss"
 "Simplification rules:
-  Pure.triv_forall_equality: (\<And>x. PROP ?V) \<equiv> PROP ?V
-  HOL.the_eq_trivial: THE x. x = ?y \<equiv> ?y
-  HOL.the_sym_eq_trivial: THE y. ?y = y \<equiv> ?y
+  Pure.triv_forall_equality: (\<And>x. PROP V) \<equiv> PROP V
+  HOL.the_eq_trivial: THE x. x = y \<equiv> y
+  HOL.the_sym_eq_trivial: THE ya. y = ya \<equiv> y
   \<dots>
 Congruences rules:
   HOL.simp_implies: \<dots>
-    \<Longrightarrow> (PROP ?P =simp=> PROP ?Q) \<equiv> (PROP ?P' =simp=> PROP ?Q')
-  op -->: \<lbrakk>?P \<equiv> ?P'; ?P' \<Longrightarrow> ?Q \<equiv> ?Q'\<rbrakk> \<Longrightarrow> ?P \<longrightarrow> ?Q \<equiv> ?P' \<longrightarrow> ?Q'"}
+    \<Longrightarrow> (PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')
+  op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'"}
 
   
   The main point of these simpsets is that they are small enough to