diff -r 8084c353d196 -r c22b507e1407 CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Fri Feb 27 15:59:38 2009 +0000
+++ b/CookBook/Tactical.thy	Sat Feb 28 14:18:02 2009 +0000
@@ -1015,7 +1015,7 @@
 
 *}
 
-section {* Simplifier Tactics *}
+section {* Simplifier Tactics (TBD) *}
 
 text {*
   A lot of convenience in the reasoning with Isabelle derives from its
@@ -1063,7 +1063,8 @@
   typical of the form
 
   \begin{isabelle}
-  \mbox{\inferrule{@{text "contr t\<^isub>1\<dots>t\<^isub>n \<equiv> contr s\<^isub>1\<dots>s\<^isub>n"}}{@{text "t\<^isub>i \<equiv> s\<^isub>i"}}}
+  \mbox{\inferrule{@{text "t\<^isub>i \<equiv> s\<^isub>i"}}
+                  {@{text "contr t\<^isub>1\<dots>t\<^isub>n \<equiv> contr s\<^isub>1\<dots>s\<^isub>n"}}}
   \end{isabelle}
 
   with @{text "constr"} being a term-constructor. However there are also more complicated 
@@ -1089,6 +1090,58 @@
   The most frequently used simpsets in HOL are @{ML HOL_basic_ss} and @{ML HOL_ss}.
 *}
 
+ML {* warning (Pretty.string_of (MetaSimplifier.pretty_ss HOL_ss)) *}
+
+ML {*
+fun get_parts ss = 
+let 
+  val ({rules, ...}, {congs, procs, loop_tacs, solvers, ...}) = MetaSimplifier.rep_ss ss
+in
+  (rules, congs, procs, loop_tacs, solvers)
+end  
+*}
+
+ML {*
+  Pretty.big_list
+*}
+
+
+ML {*
+fun print_ss ss =
+  let
+    val pretty_thms = map (enclose "  " "\n" o  Display.string_of_thm)
+
+    fun pretty_cong (name, {thm, lhs}) =
+      name ^ ":" ^ (Display.string_of_thm thm);
+
+    val (rules, congs, procs, loop_tacs, solvers) = get_parts ss;
+    val smps = map #thm (Net.entries rules);
+ 
+  in
+    "simplification rules:\n" ^ 
+       (implode (pretty_thms smps)) ^
+    "congruences:" ^ (commas (map pretty_cong (fst congs))) ^ "\n" ^
+    "loopers:" ^ (commas (map (quote o fst) loop_tacs))
+  end;
+*}
+
+thm FalseE
+
+thm simp_impliesI
+lemma "P (Suc 0) \<Longrightarrow> P ?x"
+apply(tactic {* CHANGED (simp_tac HOL_basic_ss 1) *})
+oops
+
+ML {* warning (print_ss HOL_ss) *}
+
+text {*
+  @{ML HOL_basic_ss} can deal essentially only with goals of the form: 
+  @{thm TrueI}, @{thm refl[no_vars]} @{term "x \<equiv> x"} and @{thm FalseE}, 
+  and resolve with assumptions.
+*}
+
+ML {* setsubgoaler *}
+
 text {*
   (FIXME: what do the simplifier tactics do when nothing can be rewritten)