--- a/ProgTutorial/Tactical.thy	Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Tactical.thy	Tue May 21 16:22:30 2019 +0200
@@ -1029,7 +1029,8 @@
 
 ML %grayML\<open>fun select_tac' ctxt = 
   FIRST' [resolve_tac ctxt [@{thm conjI}], resolve_tac ctxt [@{thm impI}], 
-          resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{thm allI}], K all_tac]\<close>text_raw\<open>\label{tac:selectprime}\<close>
+          resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{thm allI}],
+          K all_tac]\<close>text_raw\<open>\label{tac:selectprime}\<close>
 
 text \<open>
   Since we like to mimic the behaviour of @{ML select_tac} as closely as possible, 
@@ -1473,6 +1474,7 @@
 
 ML %grayML\<open>val ss1 = put_simpset empty_ss @{context} addsimps [@{thm Diff_Int} RS @{thm eq_reflection}]\<close>
 
+thm "INF_cong"
 text \<open>
   Printing then out the components of the simpset gives:
 
@@ -1485,10 +1487,10 @@
 
   \footnote{\bf FIXME: Why does it print out ??.unknown}
 
-  Adding also the congruence rule @{thm [source] strong_INF_cong} 
+  Adding also the congruence rule @{thm [source] INF_cong} 
 \<close>
 
-ML %grayML\<open>val ss2 = ss1 |> Simplifier.add_cong (@{thm strong_INF_cong} RS @{thm eq_reflection})\<close>
+ML %grayML\<open>val ss2 = ss1 |> Simplifier.add_cong (@{thm INF_cong} RS @{thm eq_reflection})\<close>
 
 text \<open>
   gives
@@ -1499,7 +1501,7 @@
   ??.unknown: A1 - B1 \<inter> C1 \<equiv> A1 - B1 \<union> (A1 - C1)
 Congruences rules:
   Complete_Lattices.Inf_class.Inf: 
-    \<lbrakk>A1 = B1; \<And>x. x \<in> B1 =simp=> C1 x = D1 x\<rbrakk> \<Longrightarrow> INFIMUM A1 C1 \<equiv> INFIMUM B1 D1
+    \<lbrakk>A1 = B1; \<And>x. x \<in> B1 \<Longrightarrow> C1 x = D1 x\<rbrakk> \<Longrightarrow> Inf (C1 ` A1) \<equiv> Inf (D1 ` B1)
 Simproc patterns:\<close>}
 
   Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss}