diff -r c53d74b34123 -r 638ed040e6f8 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Thu Mar 13 17:16:49 2014 +0000
+++ b/ProgTutorial/Tactical.thy	Thu Apr 03 12:16:56 2014 +0100
@@ -250,7 +250,7 @@
   form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text
   "#C"}. Since the goal @{term C} can potentially be an implication, there is a
   ``protector'' wrapped around it (the wrapper is the outermost constant
-  @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible
+  @{text "Const (\"Pure.prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible
   as a @{text #}). This wrapper prevents that premises of @{text C} are
   misinterpreted as open subgoals. While tactics can operate on the subgoals
   (the @{text "A\<^sub>i"} above), they are expected to leave the conclusion
@@ -264,7 +264,7 @@
   \begin{boxedminipage}{\textwidth}
   \begin{isabelle}
 *}
-notation (output) "prop"  ("#_" [1000] 1000)
+notation (output) "Pure.prop"  ("#_" [1000] 1000)
 
 lemma 
   shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B" 
@@ -1483,10 +1483,10 @@
 
   \footnote{\bf FIXME: Why does it print out ??.unknown}
 
-  Adding also the congruence rule @{thm [source] UN_cong} 
+  Adding also the congruence rule @{thm [source] strong_INF_cong} 
 *}
 
-ML %grayML{*val ss2 = ss1 |> Simplifier.add_cong (@{thm UN_cong} RS @{thm eq_reflection}) *}
+ML %grayML{*val ss2 = ss1 |> Simplifier.add_cong (@{thm strong_INF_cong} RS @{thm eq_reflection}) *}
 
 text {*
   gives
@@ -1496,7 +1496,8 @@
 "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
+  Complete_Lattices.Inf_class.INFIMUM: 
+    \<lbrakk>A1 = B1; \<And>x. x \<in> B1 =simp=> C1 x = D1 x\<rbrakk> \<Longrightarrow> INFIMUM A1 C1 \<equiv> INFIMUM B1 D1
 Simproc patterns:"}
 
   Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} 
@@ -2116,7 +2117,7 @@
 in
   Thm.prop_of (Thm.beta_conversion true ctrm)
 end"
-"Const (\"==\",\<dots>) $ 
+"Const (\"Pure.eq\",\<dots>) $ 
   (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ 
     (Const (\"Groups.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"}