--- a/CookBook/FirstSteps.thy	Fri Mar 06 21:52:17 2009 +0000
+++ b/CookBook/FirstSteps.thy	Sun Mar 08 20:53:00 2009 +0000
@@ -408,17 +408,14 @@
 
 ML{*fun get_thm_names_from_ss simpset =
 let
-  val ({rules,...}, _) = MetaSimplifier.rep_ss simpset
+  val {simps,...} = MetaSimplifier.dest_ss simpset
 in
-  map #name (Net.entries rules)
+  map #1 simps
 end*}
 
 text {*
-  The function @{ML rep_ss in MetaSimplifier} returns a record containing all
-  information about the simpset. The rules of a simpset are stored in a
-  \emph{discrimination net} (a data structure for fast indexing). From this
-  net you can extract the entries using the function @{ML Net.entries}.
-  You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored
+  The function @{ML dest_ss in MetaSimplifier} returns a record containing all
+  information stored in the simpset. We are only interested in the You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored
   in the current simpset. This simpset can be referred to using the antiquotation
   @{text "@{simpset}"}.
 
@@ -444,7 +441,6 @@
   course of this chapter you will learn more about these antiquotations:
   they can simplify Isabelle programming since one can directly access all
   kinds of logical elements from th ML-level.
-
 *}
 
 section {* Terms and Types *}
@@ -710,12 +706,12 @@
 text {*
   Occasional you have to calculate what the ``base'' name of a given
   constant is. For this you can use the function @{ML Sign.extern_const} or
-  @{ML NameSpace.base_name}. For example:
+  @{ML Long_Name.base_name}. For example:
 
   @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
 
   The difference between both functions is that @{ML extern_const in Sign} returns
-  the smallest name that is still unique, whereas @{ML base_name in NameSpace} always
+  the smallest name that is still unique, whereas @{ML base_name in Long_Name} always
   strips off all qualifiers.
 
   \begin{readmore}
@@ -1182,31 +1178,38 @@
 (* FIXME: some code below *)
 
 (*<*)
+(*
 setup {*
- Sign.add_consts_i [("bar", @{typ "nat"},NoSyn)] 
+ Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)] 
 *}
-
+*)
 lemma "bar = (1::nat)"
   oops
 
+(*
 setup {*   
   Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] 
  #> PureThy.add_defs false [((Binding.name "foo_def", 
        Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] 
  #> snd
 *}
-
+*)
+(*
 lemma "foo = (1::nat)"
   apply(simp add: foo_def)
   done
 
 thm foo_def
+*)
 (*>*)
 
 section {* Pretty-Printing (TBD) *}
 
 text {*
-  @{ML Pretty.big_list}
+  @{ML Pretty.big_list},
+  @{ML Pretty.brk},
+  @{ML Pretty.block},
+  @{ML Pretty.chunks}
 *}
 
 section {* Misc (TBD) *}

--- a/CookBook/Package/Ind_Code.thy	Fri Mar 06 21:52:17 2009 +0000
+++ b/CookBook/Package/Ind_Code.thy	Sun Mar 08 20:53:00 2009 +0000
@@ -3,6 +3,11 @@
 begin
 
 text {*
+  What does the @{ML Thm.internalK} do, in the LocalTheory.define Thm.internalK?
+*}
+
+
+text {*
 
   @{ML_chunk [display,gray] definitions_aux}
   @{ML_chunk [display,gray,linenos] definitions}

--- a/CookBook/Package/simple_inductive_package.ML	Fri Mar 06 21:52:17 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML	Sun Mar 08 20:53:00 2009 +0000
@@ -21,10 +21,10 @@
 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P 
 
 (* @chunk definitions_aux *) 
-fun definitions_aux s ((binding, syn), (attr, trm)) lthy =
+fun definitions_aux ((binding, syn), trm) lthy =
 let 
   val ((_, (_, thm)), lthy) = 
-                LocalTheory.define s ((binding, syn), (attr, trm)) lthy
+    LocalTheory.define Thm.internalK ((binding, syn), (Attrib.empty_binding, trm)) lthy
 in 
   (thm, lthy) 
 end
@@ -45,7 +45,7 @@
       val t2 = fold_rev mk_all preds' t1;      
       val t3 = fold_rev lambda (params @ zs) t2;
     in
-      definitions_aux Thm.internalK ((R, syn), (Attrib.empty_binding, t3))
+      definitions_aux ((R, syn), t3)
     end) (preds ~~ preds' ~~ Tss) lthy
 end
 (* @end *)

--- a/CookBook/Tactical.thy	Fri Mar 06 21:52:17 2009 +0000
+++ b/CookBook/Tactical.thy	Sun Mar 08 20:53:00 2009 +0000
@@ -1119,58 +1119,44 @@
 text_raw {*
 \begin{figure}[tp]
 \begin{isabelle}*}
-ML{*fun get_parts ss = 
-let 
-  val ({rules, ...}, {congs, procs, ...}) = MetaSimplifier.rep_ss ss
-  
-  val rules_list = Net.entries rules
-  val rnames = map #name rules_list
-  val rthms =  map #thm rules_list
-
-  val congs_list = fst congs
-  val cnames = map fst congs_list  
-  val cthms = map (#thm o snd) congs_list
-
-  val proc_list = Net.entries procs
-in
-  (rnames ~~ rthms, cnames ~~ cthms)
-end
-
-fun print_parts ctxt ss =
+ML{*fun print_ss ctxt ss =
 let
-  val (simps, congs) = get_parts ss
+  val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
 
   fun name_thm (nm, thm) =
       "  " ^ nm ^ ": " ^ (str_of_thm ctxt thm)
+  fun name_ctrm (nm, ctrm) =
+      "  " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm)
 
   val s1 = ["Simplification rules:"]
   val s2 = map name_thm simps
   val s3 = ["Congruences rules:"]
   val s4 = map name_thm congs
+  val s5 = ["Simproc patterns:"]
+  val s6 = map name_ctrm procs
 in
-  (s1 @ s2 @ s3 @ s4) 
+  (s1 @ s2 @ s3 @ s4 @ s5 @ s6) 
      |> separate "\n"
      |> implode
      |> warning
 end*}
 text_raw {* 
 \end{isabelle}
-\caption{The function @{ML MetaSimplifier.rep_ss} returns a record containing
-  a simpset. We are here only interested in the simplifcation rules, congruence rules and
-  simprocs. The first and third are discrimination nets, which from which we extract
-  lists using @{ML Net.entries}. The congruence rules are stored in 
-  an association list, associating a constant with a rule.\label{fig:prettyss}}
+\caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing
+  all printable information stored in a simpset. We are here only interested in the 
+  simplifcation rules, congruence rules and simprocs.\label{fig:printss}}
 \end{figure} *}
 
 text {* 
-  To see how they work, consider the two functions in Figure~\ref{fig:prettyss}, which
+  To see how they work, consider the two functions in Figure~\ref{fig:printss}, which
   print out some parts of a simpset. If you use them to print out the components of the
   empty simpset, in ML @{ML empty_ss} and the most primitive simpset
   
   @{ML_response_fake [display,gray]
-  "print_parts @{context} empty_ss"
+  "print_ss @{context} empty_ss"
 "Simplification rules:
-Congruences rules:"}
+Congruences rules:
+Simproc patterns:"}
 
   you can see it contains nothing. This simpset is usually not useful, except as a 
   building block to build bigger simpsets. For example you can add to @{ML empty_ss} 
@@ -1183,10 +1169,11 @@
   Printing then out the components of the simpset gives:
 
   @{ML_response_fake [display,gray]
-  "print_parts @{context} ss1"
+  "print_ss @{context} ss1"
 "Simplification rules:
   ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
-Congruences rules:"}
+Congruences rules:
+Simproc patterns:"}
 
   (FIXME: Why does it print out ??.unknown)
 
@@ -1199,11 +1186,12 @@
   gives
 
   @{ML_response_fake [display,gray]
-  "print_parts @{context} ss2"
+  "print_ss @{context} ss2"
 "Simplification rules:
   ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:
-  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"}
+  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
+Simproc patterns:"}
 
   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 
@@ -1213,9 +1201,10 @@
   printing out the components of this simpset
 
   @{ML_response_fake [display,gray]
-  "print_parts @{context} HOL_basic_ss"
+  "print_ss @{context} HOL_basic_ss"
 "Simplification rules:
-Congruences rules:"}
+Congruences rules:
+Simproc patterns:"}
 
   also produces ``nothing'', the printout is misleading. In fact
   the @{ML HOL_basic_ss} is setup so that it can solve goals of the
@@ -1239,7 +1228,7 @@
   connectives in HOL. 
 
   @{ML_response_fake [display,gray]
-  "print_parts @{context} HOL_ss"
+  "print_ss @{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
@@ -1248,7 +1237,9 @@
 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'"}
+  op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'
+Simproc patterns:
+  \<dots>"}
 
   
   The simplifier is often used to unfold definitions in a proof. For this the
@@ -1418,9 +1409,6 @@
 
   (FIXME: Is it interesting to say something about @{term "op =simp=>"}?)
 
-  (FIXME: Unfortunately one cannot access any simproc, as there is 
-  no @{text rep_proc} in function @{ML get_parts}.)
-
   (FIXME: What are the second components of the congruence rules---something to
   do with weak congruence constants?)
 

Binary file cookbook.pdf has changed