--- a/ProgTutorial/Essential.thy	Tue May 21 16:22:30 2019 +0200
+++ b/ProgTutorial/Essential.thy	Wed May 22 12:38:51 2019 +0200
@@ -2082,12 +2082,13 @@
   @{ML_response [display,gray]
   \<open>@{thm my_conjIa}
   |> get_all_names |> sort string_ord\<close>
-  \<open>["", "HOL.All_def", "HOL.FalseE", "HOL.False_def", "HOL.TrueI", "HOL.True_def", 
-   "HOL.True_or_False", "HOL.allI", "HOL.and_def", "HOL.conjI",
-   "HOL.conjunct1", "HOL.conjunct2", "HOL.disjE", "HOL.eqTrueE", "HOL.eqTrueI", 
-   "HOL.ext", "HOL.fun_cong", "HOL.iffD1", "HOL.iffD2", "HOL.iffI",
-   "HOL.impI", "HOL.mp", "HOL.or_def", "HOL.refl", "HOL.rev_iffD1", 
-   "HOL.rev_iffD2", "HOL.spec", "HOL.ssubst", "HOL.subst", "HOL.sym",
+  \<open>["", "HOL.All_def", "HOL.FalseE", "HOL.False_def", "HOL.TrueI", 
+   "HOL.True_def", "HOL.True_or_False", "HOL.allI", "HOL.and_def", 
+   "HOL.conjI", "HOL.conjunct1", "HOL.conjunct2", "HOL.disjE", 
+   "HOL.eqTrueE", "HOL.eqTrueI", "HOL.ext", "HOL.fun_cong", "HOL.iffD1", 
+   "HOL.iffD2", "HOL.iffI", "HOL.impI", "HOL.mp", "HOL.or_def", 
+   "HOL.refl", "HOL.rev_iffD1", "HOL.rev_iffD2", "HOL.spec", 
+   "HOL.ssubst", "HOL.subst", "HOL.sym",
    "Pure.protectD", "Pure.protectI"]\<close>}
 
   The theorems @{thm [source] Pure.protectD} and @{thm [source]
@@ -2112,8 +2113,9 @@
   @{ML_response [display,gray]
   \<open>@{thm my_conjIc}
   |> get_all_names\<close>
-  \<open>["HOL.simp_thms_25", "Pure.conjunctionD1", "Pure.conjunctionD2", "Pure.conjunctionI", 
-    "HOL.rev_mp", "HOL.exI", "HOL.allE", "HOL.exE",\<dots>]\<close>}
+  \<open>["HOL.simp_thms_25", "Pure.conjunctionD1", "Pure.conjunctionD2", 
+    "Pure.conjunctionI", "HOL.rev_mp", "HOL.exI", "HOL.allE", 
+    "HOL.exE",\<dots>]\<close>}
 
 
   \begin{exercise}