diff -r 72b5d28aae58 -r f58863b1406a src/HOL/TLA/Inc/Inc.ML
--- a/src/HOL/TLA/Inc/Inc.ML	Thu Aug 03 19:28:37 2000 +0200
+++ b/src/HOL/TLA/Inc/Inc.ML	Thu Aug 03 19:29:03 2000 +0200
@@ -14,37 +14,46 @@
 
 (*** Invariant proof for Psi: "manual" proof proves individual lemmas ***)
 
-qed_goal "PsiInv_Init" Inc.thy "|- InitPsi --> PsiInv"
- (fn _ => [ auto_tac (Inc_css addsimps2 InitPsi_def::PsiInv_defs) ]);
+Goal "|- InitPsi --> PsiInv";
+by (auto_tac (Inc_css addsimps2 InitPsi_def::PsiInv_defs));
+qed "PsiInv_Init";
 
-qed_goal "PsiInv_alpha1" Inc.thy "|- alpha1 & $PsiInv --> PsiInv`"
-  (fn _ => [ auto_tac (Inc_css addsimps2 alpha1_def::PsiInv_defs) ]);
+Goal "|- alpha1 & $PsiInv --> PsiInv$";
+by (auto_tac (Inc_css addsimps2 alpha1_def::PsiInv_defs));
+qed "PsiInv_alpha1";
 
-qed_goal "PsiInv_alpha2" Inc.thy "|- alpha2 & $PsiInv --> PsiInv`"
-  (fn _ => [ auto_tac (Inc_css addsimps2 alpha2_def::PsiInv_defs) ]);
+Goal "|- alpha2 & $PsiInv --> PsiInv$";
+by (auto_tac (Inc_css addsimps2 alpha2_def::PsiInv_defs));
+qed "PsiInv_alpha2";
 
-qed_goal "PsiInv_beta1" Inc.thy "|- beta1 & $PsiInv --> PsiInv`"
-  (fn _ => [ auto_tac (Inc_css addsimps2 beta1_def::PsiInv_defs) ]);
+Goal "|- beta1 & $PsiInv --> PsiInv$";
+by (auto_tac (Inc_css addsimps2 beta1_def::PsiInv_defs));
+qed "PsiInv_beta1";
 
-qed_goal "PsiInv_beta2" Inc.thy "|- beta2 & $PsiInv --> PsiInv`"
-  (fn _ => [ auto_tac (Inc_css addsimps2 beta2_def::PsiInv_defs) ]);
+Goal "|- beta2 & $PsiInv --> PsiInv$";
+by (auto_tac (Inc_css addsimps2 beta2_def::PsiInv_defs));
+qed "PsiInv_beta2";
 
-qed_goal "PsiInv_gamma1" Inc.thy "|- gamma1 & $PsiInv --> PsiInv`"
-  (fn _ => [ auto_tac (Inc_css addsimps2 gamma1_def::PsiInv_defs) ]);
+Goal "|- gamma1 & $PsiInv --> PsiInv$";
+by (auto_tac (Inc_css addsimps2 gamma1_def::PsiInv_defs));
+qed "PsiInv_gamma1";
 
-qed_goal "PsiInv_gamma2" Inc.thy "|- gamma2 & $PsiInv --> PsiInv`"
-  (fn _ => [ auto_tac (Inc_css addsimps2 gamma2_def::PsiInv_defs) ]);
+Goal "|- gamma2 & $PsiInv --> PsiInv$";
+by (auto_tac (Inc_css addsimps2 gamma2_def::PsiInv_defs));
+qed "PsiInv_gamma2";
 
-qed_goal "PsiInv_stutter" Inc.thy "|- unchanged (x,y,sem,pc1,pc2) & $PsiInv --> PsiInv`"
-  (fn _ => [ auto_tac (Inc_css addsimps2 PsiInv_defs) ]);
+Goal "|- unchanged (x,y,sem,pc1,pc2) & $PsiInv --> PsiInv$";
+by (auto_tac (Inc_css addsimps2 PsiInv_defs));
+qed "PsiInv_stutter";
 
-qed_goal "PsiInv" Inc.thy "|- Psi --> []PsiInv" (K [
-	    inv_tac (Inc_css addsimps2 [Psi_def]) 1,
-	    force_tac (Inc_css addsimps2 [PsiInv_Init, Init_def]) 1,
-	    auto_tac (Inc_css addIs2
-		        [PsiInv_alpha1,PsiInv_alpha2,PsiInv_beta1,
-			 PsiInv_beta2,PsiInv_gamma1,PsiInv_gamma2,PsiInv_stutter]
-                        addsimps2 [square_def,N1_def, N2_def]) ]);
+Goal "|- Psi --> []PsiInv";
+by (inv_tac (Inc_css addsimps2 [Psi_def]) 1);
+ by (force_tac (Inc_css addsimps2 [PsiInv_Init, Init_def]) 1);
+by (auto_tac (Inc_css
+              addIs2 [PsiInv_alpha1,PsiInv_alpha2,PsiInv_beta1,
+                      PsiInv_beta2,PsiInv_gamma1,PsiInv_gamma2,PsiInv_stutter]
+              addsimps2 [square_def,N1_def, N2_def]));
+qed "PsiInv";
 
 (* Automatic proof works too, but it make take a while on a slow machine.
    More realistic examples require user guidance anyway.
@@ -56,13 +65,14 @@
 
 (**** Step simulation ****)
 
-qed_goal "Init_sim" Inc.thy "|- Psi --> Init InitPhi"
-  (fn _ => [ auto_tac (Inc_css addsimps2 [InitPhi_def,Psi_def,InitPsi_def,Init_def]) ]);
+Goal "|- Psi --> Init InitPhi";
+by (auto_tac (Inc_css addsimps2 [InitPhi_def,Psi_def,InitPsi_def,Init_def]));
+qed "Init_sim";
 
-qed_goal "Step_sim" Inc.thy "|- Psi --> [][M1 | M2]_(x,y)"
-  (fn _ => [auto_tac (Inc_css addsimps2 [square_def,M1_def,M2_def] @ Psi_defs
-                              addSEs2 [STL4E])
-           ]);
+Goal "|- Psi --> [][M1 | M2]_(x,y)";
+by (auto_tac (Inc_css addsimps2 [square_def,M1_def,M2_def] @ Psi_defs
+                      addSEs2 [STL4E]));
+qed "Step_sim";
 
 (**** Proof of fairness ****)
 
@@ -82,166 +92,152 @@
    the auxiliary lemmas are very similar.
 *)
 
-qed_goal "Stuck_at_b" Inc.thy
-  "|- [][(N1 | N2) & ~ beta1]_(x,y,sem,pc1,pc2) --> stable(pc1 = #b)"
-  (fn _ => [ auto_tac (Inc_css addSEs2 [Stable,squareE] addsimps2 Psi_defs) ]);
+Goal "|- [][(N1 | N2) & ~ beta1]_(x,y,sem,pc1,pc2) --> stable(pc1 = #b)";
+by (auto_tac (Inc_css addSEs2 [Stable,squareE] addsimps2 Psi_defs));
+qed "Stuck_at_b";
 
-qed_goal "N1_enabled_at_g" Inc.thy
-  "|- pc1 = #g --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
-  (fn _ => [Clarsimp_tac 1,
-	    res_inst_tac [("F","gamma1")] enabled_mono 1,
-	    enabled_tac Inc_base 1,
-            force_tac (Inc_css addsimps2 [gamma1_def]) 1,
-	    force_tac (Inc_css addsimps2 [angle_def,gamma1_def,N1_def]) 1
-	   ]);
+Goal "|- pc1 = #g --> Enabled (<N1>_(x,y,sem,pc1,pc2))";
+by (Clarsimp_tac 1);
+by (res_inst_tac [("F","gamma1")] enabled_mono 1);
+by (enabled_tac Inc_base 1);
+ by (force_tac (Inc_css addsimps2 [gamma1_def]) 1);
+by (force_tac (Inc_css addsimps2 [angle_def,gamma1_def,N1_def]) 1);
+qed "N1_enabled_at_g";
 
-qed_goal "g1_leadsto_a1" Inc.thy
-  "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & []#True \
-\     --> (pc1 = #g ~> pc1 = #a)"
-  (fn _ => [rtac SF1 1,
-	    action_simp_tac (simpset() addsimps Psi_defs) [] [squareE] 1,
-	    action_simp_tac (simpset() addsimps angle_def::Psi_defs) [] [] 1,
-	    (* reduce |- []A --> <>Enabled B  to  |- A --> Enabled B *)
-	    auto_tac (Inc_css addSIs2 [InitDmd_gen, N1_enabled_at_g]
-		              addSDs2 [STL2_gen]
-		              addsimps2 [Init_def])
-	   ]);
+Goal "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & []#True \
+\        --> (pc1 = #g ~> pc1 = #a)";
+by (rtac SF1 1);
+by (action_simp_tac (simpset() addsimps Psi_defs) [] [squareE] 1);
+by (action_simp_tac (simpset() addsimps angle_def::Psi_defs) [] [] 1);
+(* reduce |- []A --> <>Enabled B  to  |- A --> Enabled B *)
+by (auto_tac (Inc_css addSIs2 [InitDmd_gen, N1_enabled_at_g]
+	              addSDs2 [STL2_gen]
+                      addsimps2 [Init_def]));
+qed "g1_leadsto_a1";
 
 (* symmetrical for N2, and similar for beta2 *)
-qed_goal "N2_enabled_at_g" Inc.thy
-  "|- pc2 = #g --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
-  (fn _ => [Clarsimp_tac 1,
-	    res_inst_tac [("F","gamma2")] enabled_mono 1,
-	    enabled_tac Inc_base 1,
-            force_tac (Inc_css addsimps2 [gamma2_def]) 1,
-	    force_tac (Inc_css addsimps2 [angle_def,gamma2_def,N2_def]) 1
-	   ]);
+Goal "|- pc2 = #g --> Enabled (<N2>_(x,y,sem,pc1,pc2))";
+by (Clarsimp_tac 1);
+by (res_inst_tac [("F","gamma2")] enabled_mono 1);
+by (enabled_tac Inc_base 1);
+ by (force_tac (Inc_css addsimps2 [gamma2_def]) 1);
+by (force_tac (Inc_css addsimps2 [angle_def,gamma2_def,N2_def]) 1);
+qed "N2_enabled_at_g";
 
-qed_goal "g2_leadsto_a2" Inc.thy
-  "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True \
-\     --> (pc2 = #g ~> pc2 = #a)"
-  (fn _ => [rtac SF1 1,
-	    action_simp_tac (simpset() addsimps Psi_defs) [] [squareE] 1,
-	    action_simp_tac (simpset() addsimps angle_def::Psi_defs) [] [] 1,
-	    auto_tac (Inc_css addSIs2 [InitDmd_gen, N2_enabled_at_g]
-		              addSDs2 [STL2_gen]
-		              addsimps2 [Init_def])
-	   ]);
+Goal "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True \
+\        --> (pc2 = #g ~> pc2 = #a)";
+by (rtac SF1 1);
+by (action_simp_tac (simpset() addsimps Psi_defs) [] [squareE] 1);
+by (action_simp_tac (simpset() addsimps angle_def::Psi_defs) [] [] 1);
+by (auto_tac (Inc_css addSIs2 [InitDmd_gen, N2_enabled_at_g]
+	              addSDs2 [STL2_gen]
+                      addsimps2 [Init_def]));
+qed "g2_leadsto_a2";
 
-qed_goal "N2_enabled_at_b" Inc.thy
-  "|- pc2 = #b --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
-  (fn _ => [Clarsimp_tac 1,
-	    res_inst_tac [("F","beta2")] enabled_mono 1,
-	    enabled_tac Inc_base 1,
-            force_tac (Inc_css addsimps2 [beta2_def]) 1,
-	    force_tac (Inc_css addsimps2 [angle_def,beta2_def,N2_def]) 1
-	   ]);
+Goal "|- pc2 = #b --> Enabled (<N2>_(x,y,sem,pc1,pc2))";
+by (Clarsimp_tac 1);
+by (res_inst_tac [("F","beta2")] enabled_mono 1);
+by (enabled_tac Inc_base 1);
+ by (force_tac (Inc_css addsimps2 [beta2_def]) 1);
+by (force_tac (Inc_css addsimps2 [angle_def,beta2_def,N2_def]) 1);
+qed "N2_enabled_at_b";
 
-qed_goal "b2_leadsto_g2" Inc.thy
-  "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True \
-\     --> (pc2 = #b ~> pc2 = #g)"
-  (fn _ => [rtac SF1 1,
-	    action_simp_tac (simpset() addsimps Psi_defs) [] [squareE] 1,
-	    action_simp_tac (simpset() addsimps angle_def::Psi_defs) [] [] 1,
-	    auto_tac (Inc_css addSIs2 [InitDmd_gen, N2_enabled_at_b]
-		              addSDs2 [STL2_gen]
-		              addsimps2 [Init_def])
-	   ]);
+Goal "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True \
+\        --> (pc2 = #b ~> pc2 = #g)";
+by (rtac SF1 1);
+by (action_simp_tac (simpset() addsimps Psi_defs) [] [squareE] 1);
+by (action_simp_tac (simpset() addsimps angle_def::Psi_defs) [] [] 1);
+by (auto_tac (Inc_css addSIs2 [InitDmd_gen, N2_enabled_at_b]
+                      addSDs2 [STL2_gen]
+                      addsimps2 [Init_def]));
+qed "b2_leadsto_g2";
 
 (* Combine above lemmas: the second component will eventually reach pc2 = a *)
-qed_goal "N2_leadsto_a" Inc.thy
-  "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True \
-\     --> (pc2 = #a | pc2 = #b | pc2 = #g ~> pc2 = #a)"
-  (fn _ => [auto_tac (Inc_css addSIs2 [LatticeDisjunctionIntro]),
-	    rtac (temp_use LatticeReflexivity) 1,
-	    rtac (temp_use LatticeTransitivity) 1,
-	    auto_tac (Inc_css addSIs2 [b2_leadsto_g2,g2_leadsto_a2])
-	   ]);
+Goal "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True \
+\        --> (pc2 = #a | pc2 = #b | pc2 = #g ~> pc2 = #a)";
+by (auto_tac (Inc_css addSIs2 [LatticeDisjunctionIntro]));
+by (rtac (temp_use LatticeReflexivity) 1);
+by (rtac (temp_use LatticeTransitivity) 1);
+by (auto_tac (Inc_css addSIs2 [b2_leadsto_g2,g2_leadsto_a2]));
+qed "N2_leadsto_a";
 
-(* Get rid of complete disjunction on the left-hand side of ~> above. *)
-qed_goal "N2_live" Inc.thy
-  "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) \
-\     --> <>(pc2 = #a)"
-  (fn _ => [auto_tac (Inc_css addsimps2 Init_defs
-                              addSIs2 [(temp_use N2_leadsto_a) 
-                                       RSN(2, (temp_use leadsto_init))]),
-	    case_tac "pc2 (st1 sigma)" 1,
-	    Auto_tac
-	   ]);
+(* Get rid of disjunction on the left-hand side of ~> above. *)
+Goal "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) \
+\        --> <>(pc2 = #a)";
+by (auto_tac (Inc_css addsimps2 Init_defs
+                      addSIs2 [(temp_use N2_leadsto_a) 
+                               RSN(2, (temp_use leadsto_init))]));
+by (case_tac "pc2 (st1 sigma)" 1);
+by Auto_tac;
+qed "N2_live";
 
 (* Now prove that the first component will eventually reach pc1 = b from pc1 = a *)
 
-qed_goal "N1_enabled_at_both_a" Inc.thy
-  "|- pc2 = #a & (PsiInv & pc1 = #a) --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
-  (fn _ => [Clarsimp_tac 1,
-	    res_inst_tac [("F","alpha1")] enabled_mono 1,
-	    enabled_tac Inc_base 1,
-            force_tac (Inc_css addsimps2 (alpha1_def::PsiInv_defs)) 1,
-	    force_tac (Inc_css addsimps2 [angle_def,alpha1_def,N1_def]) 1
-	   ]);
+Goal "|- pc2 = #a & (PsiInv & pc1 = #a) --> Enabled (<N1>_(x,y,sem,pc1,pc2))";
+by (Clarsimp_tac 1);
+by (res_inst_tac [("F","alpha1")] enabled_mono 1);
+by (enabled_tac Inc_base 1);
+ by (force_tac (Inc_css addsimps2 (alpha1_def::PsiInv_defs)) 1);
+by (force_tac (Inc_css addsimps2 [angle_def,alpha1_def,N1_def]) 1);
+qed "N1_enabled_at_both_a";
 
-qed_goal "a1_leadsto_b1" Inc.thy
-  "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))            \
-\           & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)  \
-\     --> (pc1 = #a ~> pc1 = #b)"
-  (fn _ => [rtac SF1 1,
-            action_simp_tac (simpset() addsimps Psi_defs) [] [squareE] 1,
-            action_simp_tac (simpset() addsimps angle_def::Psi_defs) [] [] 1,
-	    clarsimp_tac (Inc_css addSIs2 [N1_enabled_at_both_a RS (temp_use DmdImpl)]) 1,
-	    auto_tac (Inc_css addSIs2 [BoxDmd2_simple, N2_live]
-		              addsimps2 split_box_conj::more_temp_simps)
-	   ]);
+Goal "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))      \
+\        & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)  \
+\        --> (pc1 = #a ~> pc1 = #b)";
+by (rtac SF1 1);
+by (action_simp_tac (simpset() addsimps Psi_defs) [] [squareE] 1);
+by (action_simp_tac (simpset() addsimps angle_def::Psi_defs) [] [] 1);
+by (clarsimp_tac (Inc_css addSIs2 [N1_enabled_at_both_a RS (temp_use DmdImpl)]) 1);
+by (auto_tac (Inc_css addSIs2 [BoxDmd2_simple, N2_live]
+	              addsimps2 split_box_conj::more_temp_simps));
+qed "a1_leadsto_b1";
 
 (* Combine the leadsto properties for N1: it will arrive at pc1 = b *)
 
-qed_goal "N1_leadsto_b" Inc.thy
-  "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))             \
-\            & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)  \
-\     --> (pc1 = #b | pc1 = #g | pc1 = #a ~> pc1 = #b)"
-  (fn _ => [auto_tac (Inc_css addSIs2 [LatticeDisjunctionIntro]),
-	    rtac (temp_use LatticeReflexivity) 1,
-	    rtac (temp_use LatticeTransitivity) 1,
-	    auto_tac (Inc_css addSIs2 [a1_leadsto_b1,g1_leadsto_a1]
-		              addsimps2 [split_box_conj])
-	   ]);
+Goal "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))             \
+\        & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)  \
+\        --> (pc1 = #b | pc1 = #g | pc1 = #a ~> pc1 = #b)";
+by (auto_tac (Inc_css addSIs2 [LatticeDisjunctionIntro]));
+by (rtac (temp_use LatticeReflexivity) 1);
+by (rtac (temp_use LatticeTransitivity) 1);
+by (auto_tac (Inc_css addSIs2 [a1_leadsto_b1,g1_leadsto_a1]
+	              addsimps2 [split_box_conj]));
+qed "N1_leadsto_b";
 
-qed_goal "N1_live" Inc.thy
-  "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))             \
-\            & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)  \
-\     --> <>(pc1 = #b)"
-  (fn _ => [auto_tac (Inc_css addsimps2 Init_defs
-                              addSIs2 [(temp_use N1_leadsto_b) 
-                                       RSN(2, temp_use leadsto_init)]),
-	    case_tac "pc1 (st1 sigma)" 1,
-	    Auto_tac
-	   ]);
+Goal "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))             \
+\        & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)  \
+\        --> <>(pc1 = #b)";
+by (auto_tac (Inc_css addsimps2 Init_defs
+                      addSIs2 [(temp_use N1_leadsto_b) 
+                               RSN(2, temp_use leadsto_init)]));
+by (case_tac "pc1 (st1 sigma)" 1);
+by Auto_tac;
+qed "N1_live";
 
-qed_goal "N1_enabled_at_b" Inc.thy
-  "|- pc1 = #b --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
-  (fn _ => [Clarsimp_tac 1,
-	    res_inst_tac [("F","beta1")] enabled_mono 1,
-	    enabled_tac Inc_base 1,
-            force_tac (Inc_css addsimps2 [beta1_def]) 1,
-	    force_tac (Inc_css addsimps2 [angle_def,beta1_def,N1_def]) 1
-	   ]);
+Goal "|- pc1 = #b --> Enabled (<N1>_(x,y,sem,pc1,pc2))";
+by (Clarsimp_tac 1);
+by (res_inst_tac [("F","beta1")] enabled_mono 1);
+by (enabled_tac Inc_base 1);
+ by (force_tac (Inc_css addsimps2 [beta1_def]) 1);
+by (force_tac (Inc_css addsimps2 [angle_def,beta1_def,N1_def]) 1);
+qed "N1_enabled_at_b";
 
 (* Now assemble the bits and pieces to prove that Psi is fair. *)
 
-qed_goal "Fair_M1_lemma" Inc.thy
-  "|- []($PsiInv & [(N1 | N2)]_(x,y,sem,pc1,pc2))   \
-\     & SF(N1)_(x,y,sem,pc1,pc2) & []SF(N2)_(x,y,sem,pc1,pc2)  \
-\     --> SF(M1)_(x,y)"
-  (fn _ => [ res_inst_tac [("B","beta1"),("P","PRED pc1 = #b")] SF2 1,
-               (* action premises *)
-             force_tac (Inc_css addsimps2 [angle_def,M1_def,beta1_def]) 1,
-             force_tac (Inc_css addsimps2 angle_def::Psi_defs) 1,
-             force_tac (Inc_css addSEs2 [N1_enabled_at_b]) 1,
-               (* temporal premise: use previous lemmas and simple TL *)
-             force_tac (Inc_css addSIs2 [DmdStable, N1_live,Stuck_at_b] 
-                                addEs2 [STL4E] addsimps2 [square_def]) 1
-            ]);
+Goal "|- []($PsiInv & [(N1 | N2)]_(x,y,sem,pc1,pc2))   \
+\        & SF(N1)_(x,y,sem,pc1,pc2) & []SF(N2)_(x,y,sem,pc1,pc2)  \
+\        --> SF(M1)_(x,y)";
+by (res_inst_tac [("B","beta1"),("P","PRED pc1 = #b")] SF2 1);
+   (* action premises *)
+by (force_tac (Inc_css addsimps2 [angle_def,M1_def,beta1_def]) 1);
+by (force_tac (Inc_css addsimps2 angle_def::Psi_defs) 1);
+by (force_tac (Inc_css addSEs2 [N1_enabled_at_b]) 1);
+   (* temporal premise: use previous lemmas and simple TL *)
+by (force_tac (Inc_css addSIs2 [DmdStable, N1_live,Stuck_at_b] 
+                       addEs2 [STL4E] addsimps2 [square_def]) 1);
+qed "Fair_M1_lemma";
 
-qed_goal "Fair_M1" Inc.thy "|- Psi --> WF(M1)_(x,y)"
-  (fn _ => [auto_tac (Inc_css addSIs2 [SFImplWF, Fair_M1_lemma, PsiInv]
-		              addsimps2 [Psi_def,split_box_conj]@more_temp_simps)
-	   ]);
+Goal "|- Psi --> WF(M1)_(x,y)";
+by (auto_tac (Inc_css addSIs2 [SFImplWF, Fair_M1_lemma, PsiInv]
+		      addsimps2 [Psi_def,split_box_conj]@more_temp_simps));
+qed "Fair_M1";