--- a/ProgTutorial/Package/Ind_Prelims.thy	Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Package/Ind_Prelims.thy	Tue May 21 16:22:30 2019 +0200
@@ -117,8 +117,8 @@
   by starting a subproof.
 \<close>
 
+  subgoal premises for P
 proof -
-  case (goal1 P)
   have p1: "R x y" by fact
   have p2: "\<forall>P. (\<forall>x. P x x) 
                   \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P y z" by fact
@@ -155,6 +155,7 @@
     apply(rule p2[THEN spec[where x=P], THEN mp, THEN mp, OF r1, OF r2])
     done
 qed
+done
 
 text \<open>
   Now we are done. It might be surprising that we are not using the automatic
@@ -231,8 +232,8 @@
 shows "odd m \<Longrightarrow> even (Suc m)"
 apply (unfold odd_def even_def)
 apply (rule allI impI)+
+subgoal premises for P Q
 proof -
-  case (goal1 P Q)
   have p1: "\<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 
                              \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q m" by fact
   have r1: "P 0" by fact
@@ -244,6 +245,7 @@
 	           THEN mp, THEN mp, THEN mp, OF r1, OF r2, OF r3])
     done
 qed
+done
 
 text \<open>
   The interesting lines are 7 to 15. Again, the assumptions fall into two categories:
@@ -280,21 +282,23 @@
 shows "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
 apply (unfold accpart_def)
 apply (rule allI impI)+
+subgoal premises for P
 proof -
-  case (goal1 P)
   have p1: "\<And>y. R y x \<Longrightarrow> 
                    (\<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P y)" by fact
   have r1: "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x" by fact
   show "P x"
     apply(rule r1[rule_format])
+    subgoal premises for y
     proof -
-      case (goal1 y)
       have r1_prem: "R y x" by fact
       show "P y"
-	apply(rule p1[OF r1_prem, THEN spec[where x=P], THEN mp, OF r1])
+	    apply(rule p1[OF r1_prem, THEN spec[where x=P], THEN mp, OF r1])
       done
-  qed
+    qed
+    done
 qed
+done
 
 text \<open>
   As you can see, there are now two subproofs. The assumptions fall as usual into