# HG changeset patch
# User oheimb
# Date 909167719 -7200
# Node ID 22081de4125441ed0b3a42a57503a0791f5d40ce
# Parent  98744e38ded1a03f693534a925b3b8e1317a908e
corrected auto_tac (applications of unsafe wrappers)
improved style of several proofs

diff -r 98744e38ded1 -r 22081de41254 src/HOL/TLA/Buffer/DBuffer.ML
--- a/src/HOL/TLA/Buffer/DBuffer.ML	Fri Oct 23 20:34:59 1998 +0200
+++ b/src/HOL/TLA/Buffer/DBuffer.ML	Fri Oct 23 20:35:19 1998 +0200
@@ -87,8 +87,8 @@
   "[][DBNext]_<inp,mid,out,q1,q2> .& WF(DBPass)_<inp,mid,out,q1,q2> \
 \  .-> ($Enabled (<Deq inp qc out>_<inp,qc,out>) ~> $q2 .~= .[])";
 by (auto_tac (temp_css addSIs2 [leadsto_classical] addSEs2 [temp_conjimpE DBFair_1a]));
-by (auto_tac (temp_css addsimps2 [leadsto,Init_def] addDs2 [STL2bD]
-                       addSDs2 [action_mp Deq_enabledE] addSEs2 [STL4E]));
+by (force_tac (temp_css addsimps2 [leadsto,Init_def] addDs2 [STL2bD]
+                        addSDs2 [action_mp Deq_enabledE] addSEs2 [STL4E]) 1);
 qed "DBFair_1";
 
 (* Condition (2) *)
diff -r 98744e38ded1 -r 22081de41254 src/HOL/TLA/Inc/Inc.ML
--- a/src/HOL/TLA/Inc/Inc.ML	Fri Oct 23 20:34:59 1998 +0200
+++ b/src/HOL/TLA/Inc/Inc.ML	Fri Oct 23 20:35:19 1998 +0200
@@ -38,16 +38,15 @@
 qed_goal "PsiInv_stutter" Inc.thy "unchanged <x,y,sem,pc1,pc2> .& PsiInv .-> PsiInv`"
   (fn _ => [ auto_tac (Inc_css addsimps2 PsiInv_defs) ]);
 
-qed_goal "PsiInv" Inc.thy "Psi .-> []PsiInv"
-  (fn _ => [inv_tac (Inc_css addsimps2 [Psi_def]) 1,
+qed_goal "PsiInv" Inc.thy "Psi .-> []PsiInv" (K [
+	    inv_tac (Inc_css addsimps2 [Psi_def]) 1,
 	    SELECT_GOAL (auto_tac (Inc_css addSIs2 [action_mp PsiInv_Init]
 				           addsimps2 [Init_def])) 1,
-	    auto_tac (Inc_css addSEs2 (map action_conjimpE
-				           [PsiInv_alpha1,PsiInv_alpha2,PsiInv_beta1,
-					    PsiInv_beta2,PsiInv_gamma1,PsiInv_gamma2])
-		              addIs2 [action_mp PsiInv_stutter]
-                              addsimps2 [square_def,N1_def, N2_def])
-	   ]);
+	    force_tac (Inc_css addSEs2 (map action_conjimpE
+				   [PsiInv_alpha1,PsiInv_alpha2,PsiInv_beta1,
+				    PsiInv_beta2,PsiInv_gamma1,PsiInv_gamma2])
+		               addIs2 [action_mp PsiInv_stutter]
+                               addsimps2 [square_def,N1_def, N2_def]) 1]);
 
 
 
diff -r 98744e38ded1 -r 22081de41254 src/HOL/TLA/Memory/Memory.ML
--- a/src/HOL/TLA/Memory/Memory.ML	Fri Oct 23 20:34:59 1998 +0200
+++ b/src/HOL/TLA/Memory/Memory.ML	Fri Oct 23 20:35:19 1998 +0200
@@ -64,7 +64,7 @@
 
 qed_goal "MemReturn_change" Memory.thy
    "MemReturn ch rs p .-> <MemReturn ch rs p>_<rtrner ch @ p, rs@p>"
-   (fn _ => [ auto_tac (action_css addsimps2 [MemReturn_def,angle_def]) ]);
+   (K [ force_tac (action_css addsimps2 [MemReturn_def,angle_def]) 1]);
 
 qed_goal "MemReturn_enabled" Memory.thy
    "!!p. base_var <rtrner ch @ p, rs@p> ==> \
diff -r 98744e38ded1 -r 22081de41254 src/HOL/TLA/TLA.ML
--- a/src/HOL/TLA/TLA.ML	Fri Oct 23 20:34:59 1998 +0200
+++ b/src/HOL/TLA/TLA.ML	Fri Oct 23 20:35:19 1998 +0200
@@ -118,7 +118,7 @@
 
 (* ------------------------ STL3 ------------------------------------------- *)
 qed_goal "STL3" TLA.thy "([][]F) .= ([]F)"
-   (fn _ => [auto_tac (temp_css addIs2 [temp_mp transT,temp_mp STL2])]);
+   (K [force_tac (temp_css addIs2 [temp_mp transT,temp_mp STL2]) 1]);
 
 (* corresponding elimination rule introduces double boxes: 
    [| (sigma |= []F); (sigma |= [][]F) ==> PROP W |] ==> PROP W
@@ -403,7 +403,7 @@
 	     rewrite_goals_tac more_temp_simps,
 	     etac (temp_conjimpE STL6) 1, atac 1,
 	     subgoal_tac "sigma |= <>[].~F" 1,
-	     SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
+	     force_tac (temp_css addsimps2 [dmd_def]) 1,
 	     fast_tac (temp_cs addEs [DmdImplE,STL4E]) 1
 	    ]);
 
@@ -450,7 +450,7 @@
 
 qed_goalw "INV1" TLA.thy [stable_def,boxact_def] 
   "Init(P) .& stable(P) .-> []P"
-  (fn _ => [auto_tac (temp_css addsimps2 Init_simps addEs2 [ind_rule])]);
+  (K [force_tac (temp_css addsimps2 Init_simps addEs2 [ind_rule]) 1]);
 bind_thm("INV1I", temp_conjmp INV1);
 
 qed_goalw "StableL" TLA.thy [stable_def]
@@ -478,8 +478,7 @@
 (* ---------------- (Semi-)automatic invariant tactics ---------------------- *)
 
 (* inv_tac reduces goals of the form ... ==> sigma |= []P *)
-fun inv_tac css =
-   SELECT_GOAL
+fun inv_tac css = SELECT_GOAL
      (EVERY [auto_tac css,
              TRY (merge_box_tac 1),
              rtac INV1I 1, (* fail if the goal is not a box *)
@@ -492,8 +491,7 @@
    too late.
 *)
 
-fun auto_inv_tac ss =
-  SELECT_GOAL
+fun auto_inv_tac ss = SELECT_GOAL
     ((inv_tac (claset(),ss) 1) THEN
      (TRYALL (action_simp_tac (ss addsimps [Init_def,square_def]) [] [])));
 
@@ -516,20 +514,19 @@
 	     auto_tac (temp_css addsimps2 [stable_def] addSEs2 [INV1I,STL4E])
 	    ]);
 
-qed_goalw "DmdRec" TLA.thy [dmd_def] "(<>$P) .= (Init($P) .| (<>P$))"
-   (fn _ => [Auto_tac,
+qed_goalw "DmdRec" TLA.thy [dmd_def] "(<>$P) .= (Init($P) .| (<>P$))" (K [
+	     Auto_tac,
 	     etac notE 1,
-	     SELECT_GOAL (auto_tac (temp_css addsimps2 (stable_def::Init_simps)
-				             addIs2 [INV1I] addEs2 [STL4E])) 1,
-	     SELECT_GOAL (auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2bD])) 1,
+	     force_tac (temp_css addsimps2 (stable_def::Init_simps)
+				             addIs2 [INV1I] addEs2 [STL4E]) 1,
+	     force_tac (temp_css addsimps2 Init_simps addSDs2 [STL2bD]) 1,
 	     fast_tac (temp_cs addSEs [notE,TLA2E]) 1
 	    ]);
 
 qed_goal "DmdRec2" TLA.thy
-   "!!sigma. [| (sigma |= <>($P)); (sigma |= [](.~P$)) |] ==> (sigma |= Init($P))"
-   (fn _ => [dtac ((temp_unlift DmdRec) RS iffD1) 1,
-	     SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1
-	    ]);
+ "!!sigma. [| (sigma |= <>($P)); (sigma |= [](.~P$)) |] ==> (sigma |= Init($P))"
+   (K [      dtac ((temp_unlift DmdRec) RS iffD1) 1,
+	     force_tac (temp_css addsimps2 [dmd_def]) 1]);
 
 (* The "=>" part of the following is a little intricate. *)
 qed_goal "InfinitePrime" TLA.thy "([]<>$P) .= ([]<>P$)"
@@ -539,9 +536,9 @@
 	     subgoal_tac "sigma |= <>[]$P" 1,
 	     fast_tac (temp_cs addSEs [DmdImplE,TLA2E]) 1,
 	     subgoal_tac "sigma |= <>[](<>$P .& [].~P$)" 1,
-	     SELECT_GOAL (auto_tac (temp_css addsimps2 [boxact_def]
-				             addSEs2 [DmdImplE,STL4E,DmdRec2])) 1,
-	     SELECT_GOAL (auto_tac (temp_css addSIs2 [temp_mp STL6] addsimps2 more_temp_simps)) 1,
+	     force_tac (temp_css addsimps2 [boxact_def]
+			             addSEs2 [DmdImplE,STL4E,DmdRec2]) 1,
+	     force_tac (temp_css addSIs2 [temp_mp STL6] addsimps2 more_temp_simps) 1,
 	     fast_tac (temp_cs addIs [temp_mp DmdPrime] addSEs [STL4E]) 1
 	    ]);
 
@@ -591,12 +588,12 @@
    (fn _ => [ fast_tac (temp_cs addSDs [temp_mp STL2]) 1 ]);
 
 qed_goalw "streett_leadsto" TLA.thy [leadsto]
-   "([]<>P .-> []<>Q) .= (<>(P ~> Q))"
-   (fn _ => [Auto_tac,
+   "([]<>P .-> []<>Q) .= (<>(P ~> Q))" (K [
+             Auto_tac,
              asm_full_simp_tac (simpset() addsimps boxact_def::more_temp_simps) 1,
-             SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImplE,STL4E] 
-                                             addsimps2 Init_simps)) 1,
-             SELECT_GOAL (auto_tac (temp_css addSIs2 [ImplDmdD] addSEs2 [STL4E])) 1,
+             force_tac (temp_css addSEs2 [DmdImplE,STL4E] 
+                                             addsimps2 Init_simps) 1,
+             force_tac (temp_css addSIs2 [ImplDmdD] addSEs2 [STL4E]) 1,
              subgoal_tac "sigma |= []<><>Q" 1,
              asm_full_simp_tac (simpset() addsimps more_temp_simps) 1,
              rewtac (temp_rewrite DmdAct),
@@ -648,21 +645,21 @@
 	    ]);
 
 qed_goal "EnsuresLeadsto" TLA.thy
-   "A .& P .-> Q` ==> []A .-> (P ~> Q)"
-   (fn [prem] => [auto_tac (temp_css addSEs2 [INV_leadsto]),
+   "A .& P .-> Q` ==> []A .-> (P ~> Q)" (fn [prem] => [
+		  auto_tac (temp_css addSEs2 [INV_leadsto]),
 		  rewtac leadsto,
  		  auto_tac (temp_css addSIs2 [temp_unlift necT]),
-		  rtac (temp_mp DmdPrime) 1, rtac InitDmdD 1,
-		  auto_tac (action_css addsimps2 [Init_def] addSIs2 [action_mp prem])
-		 ]);
+		  rtac (temp_mp DmdPrime) 1, 
+		  rtac InitDmdD 1,
+		  force_tac (action_css addsimps2 [Init_def] 
+				addSIs2 [action_mp prem]) 1]);
 
 qed_goalw "EnsuresLeadsto2" TLA.thy [leadsto]
    "!!sigma. sigma |= [](P .-> Q`) ==> sigma |= P ~> Q"
    (fn _ => [subgoal_tac "sigma |= []Init(P .-> Q`)" 1,
              etac STL4E 1,
-             auto_tac (temp_css addsimps2 boxact_def::Init_simps 
-                                addIs2 [(temp_mp InitDmd) RS (temp_mp DmdPrime)])
-            ]);
+             ALLGOALS (force_tac (temp_css addsimps2 boxact_def::Init_simps 
+                          addIs2 [(temp_mp InitDmd) RS (temp_mp DmdPrime)]))]);
              
 qed_goal "EnsuresInfinite" TLA.thy
    "[| (sigma |= []<>P); (sigma |= []A); A .& P .-> Q` |] ==> (sigma |= []<>Q)"
@@ -722,9 +719,8 @@
    "[| P .& N  .-> P` .| Q`;   \
 \      P .& N .& <A>_v .-> Q`;   \
 \      P .& N .-> $(Enabled(<A>_v)) |]   \
-\  ==> []N .& WF(A)_v .-> (P ~> Q)"
-   (fn [prem1,prem2,prem3]
-	 => [auto_tac (temp_css addSDs2 [BoxWFI]),
+\  ==> []N .& WF(A)_v .-> (P ~> Q)"  (fn [prem1,prem2,prem3] => [
+	     auto_tac (temp_css addSDs2 [BoxWFI]),
 	     etac STL4Edup 1, atac 1,
 	     Auto_tac,
 	     subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
@@ -737,9 +733,9 @@
 	     atac 2,
 	     subgoal_tac "sigmaa |= [][]$(Enabled(<A>_v))" 1,
 	     merge_box_tac 1,
-	     SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
-	     SELECT_GOAL ((rewtac (temp_rewrite STL3)) THEN
-			  (auto_tac (temp_css addSEs2 [STL4E] addSIs2 [action_mp prem3]))) 1,
+	     force_tac (temp_css addsimps2 [dmd_def]) 1,
+	     SELECT_GOAL (rewtac (temp_rewrite STL3)) 1,
+	     force_tac (temp_css addSEs2 [STL4E] addSIs2 [action_mp prem3]) 1,
 	     fast_tac (action_cs addSIs [action_mp prem2]) 1,
 	     fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1,
 	     fast_tac (temp_cs addSEs [STL4E] addSIs [action_mp prem1]) 1
@@ -756,7 +752,7 @@
            etac STL4Edup 1, atac 1,
            Auto_tac,
            subgoal_tac "sigmaa |= <><A>_v" 1,
-           SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImpl2,STL4E] addSIs2 [action_mp prem2])) 1,
+           force_tac (temp_css addSEs2 [DmdImpl2,STL4E] addSIs2 [action_mp prem2]) 1,
            rtac classical 1,
            rtac STL2D 1,
            auto_tac (temp_css addsimps2 WF_def::more_temp_simps addSEs2 [mp]),
@@ -788,7 +784,7 @@
 		 SELECT_GOAL (old_auto_tac (temp_css addsimps2 [SF_alt])) 1,
 		 atac 2,
 		 subgoal_tac "sigmaa |= []<>$(Enabled(<A>_v))" 1,
-		 SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
+		 force_tac (temp_css addsimps2 [dmd_def]) 1,
 		 eres_inst_tac [("F","F")] dup_boxE 1,
 		 etac STL4Edup 1, atac 1,
 		 fast_tac (temp_cs addSEs [STL4E] addSIs [temp_mp prem3]) 1,
@@ -802,11 +798,10 @@
 \      P .& P` .& <N .& A>_f .-> B;   \
 \      P .& $(Enabled(<M>_g)) .-> $(Enabled(<A>_f));   \
 \      [](N .& [.~B]_f) .& WF(A)_f .& []F .& <>[]($(Enabled(<M>_g))) .-> <>[]P |]   \
-\  ==> []N .& WF(A)_f .& []F .-> WF(M)_g"
-   (fn [prem1,prem2,prem3,prem4]
-       => [Auto_tac,
+\  ==> []N .& WF(A)_f .& []F .-> WF(M)_g" (fn [prem1,prem2,prem3,prem4] => [
+	   Auto_tac,
 	   case_tac "sigma |= <>[]$Enabled(<M>_g)" 1,
-	   SELECT_GOAL (auto_tac (temp_css addsimps2 [WF_def,dmd_def])) 2,
+	    force_tac (temp_css addsimps2 [WF_def,dmd_def]) 2,
 	   case_tac "sigma |= <>[][.~B]_f" 1,
 	   subgoal_tac "sigma |= <>[]P" 1,
 	   asm_full_simp_tac (simpset() addsimps [WF_def]) 1,
@@ -822,11 +817,11 @@
 	   dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1,
 	   merge_act_box_tac 1,
 	   etac InfImpl 1, atac 1,
-	   SELECT_GOAL (auto_tac (temp_css addsimps2 [angle_def] addSIs2 [action_mp prem2])) 1,
+	   force_tac (temp_css addsimps2 [angle_def]addSIs2[action_mp prem2]) 1,
 	   etac BoxDmd 1,
 	   dres_inst_tac [("F","<><A>_f"),("G","[]P")] BoxDmd 1, atac 1,
 	   eres_inst_tac [("F","[]<><A>_f .& []P")] DmdImplE 1,
-	   SELECT_GOAL Auto_tac 1,
+	   Force_tac 1,
 	   rtac (temp_mp (prem3 RS STL4 RS DmdImpl)) 1,
 	   fast_tac (temp_cs addIs [STL4E,DmdImplE]) 1,
 	   etac (temp_conjimpE STL6) 1, atac 1,
@@ -840,12 +835,11 @@
 	   rtac dup_dmdD 1,
 	   rtac (temp_mp (prem4 RS DmdImpl)) 1,
 	   etac DmdImplE 1,
-	   SELECT_GOAL
-	     (auto_tac (temp_css addsimps2 [symmetric(temp_rewrite STL5), temp_rewrite STL3]
-		                 addIs2 [(temp_unlift WF_Box) RS iffD1, temp_mp ImplDmd])) 1,
+	   force_tac (temp_css addsimps2 [symmetric(temp_rewrite STL5), temp_rewrite STL3]
+		                 addIs2 [(temp_unlift WF_Box) RS iffD1, temp_mp ImplDmd]) 1,
 	   asm_full_simp_tac (simpset() addsimps (WF_def::more_temp_simps)) 1,
 	   etac InfImpl 1, atac 1,
-	   SELECT_GOAL (auto_tac (temp_css addSIs2 [action_mp prem1])) 1,
+	   auto_tac (temp_css addSIs2 [action_mp prem1]),
 	   ALLGOALS (asm_full_simp_tac (simpset() addsimps [square_def,angle_def]))
 	  ]);
 
@@ -854,11 +848,10 @@
 \      P .& P` .& <N .& A>_f .-> B;   \
 \      P .& $(Enabled(<M>_g)) .-> $(Enabled(<A>_f));   \
 \      [](N .& [.~B]_f) .& SF(A)_f .& []F .& []<>($(Enabled(<M>_g))) .-> <>[]P |]   \
-\  ==> []N .& SF(A)_f .& []F .-> SF(M)_g"
-   (fn [prem1,prem2,prem3,prem4]
-       => [Auto_tac,
+\  ==> []N .& SF(A)_f .& []F .-> SF(M)_g" (fn [prem1,prem2,prem3,prem4] => [
+	   Auto_tac,
 	   case_tac "sigma |= []<>$Enabled(<M>_g)" 1,
-	   SELECT_GOAL (auto_tac (temp_css addsimps2 [SF_def,dmd_def])) 2,
+	   force_tac (temp_css addsimps2 [SF_def,dmd_def]) 2,
 	   case_tac "sigma |= <>[][.~B]_f" 1,
 	   subgoal_tac "sigma |= <>[]P" 1,
 	   asm_full_simp_tac (simpset() addsimps [SF_def]) 1,
@@ -874,11 +867,11 @@
 	   dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1,
 	   merge_act_box_tac 1,
 	   etac InfImpl 1, atac 1,
-	   SELECT_GOAL (auto_tac (temp_css addsimps2 [angle_def] addSIs2 [action_mp prem2])) 1,
+	   force_tac (temp_css addsimps2 [angle_def]addSIs2[action_mp prem2]) 1,
 	   etac BoxDmd 1,
 	   dres_inst_tac [("F","<><A>_f"),("G","[]P")] BoxDmd 1, atac 1,
 	   eres_inst_tac [("F","[]<><A>_f .& []P")] DmdImplE 1,
-	   SELECT_GOAL Auto_tac 1,
+	   Force_tac 1,
 	   rtac (temp_mp (prem3 RS DmdImpl RS STL4)) 1,
 	   fast_tac (temp_cs addEs [STL4E,DmdImplE]) 1,
 	   dtac BoxSFI 1,
@@ -886,16 +879,16 @@
 	   eres_inst_tac [("F","F")] dup_boxE 1,
 	   eres_inst_tac [("F","<>$Enabled (<M>_g)")] dup_boxE 1,
 	   merge_temp_box_tac 1,
-	   dtac (temp_conjmp BoxDmdT2) 1, atac 1,
+	   dtac (temp_conjmp BoxDmdT2) 1 THEN atac 1,
 	   rtac dup_dmdD 1,
 	   rtac (temp_mp (prem4 RS DmdImpl)) 1,
-	   SELECT_GOAL
-	     (auto_tac (temp_css addsimps2 [symmetric(temp_rewrite STL5), temp_rewrite STL3]
-		                 addIs2 [(temp_unlift WF_Box) RS iffD1, temp_mp ImplDmd]
-			         addSEs2 [DmdImplE])) 1,
+	   force_tac (temp_css 
+		addsimps2 [symmetric(temp_rewrite STL5), temp_rewrite STL3]
+		addSIs2 [(temp_unlift WF_Box) RS iffD1, temp_mp ImplDmd]
+		addSEs2 [DmdImplE]) 1,
 	   asm_full_simp_tac (simpset() addsimps (SF_def::more_temp_simps)) 1,
-	   eres_inst_tac [("F",".~ [.~ B]_f")] InfImpl 1, atac 1,
-	   SELECT_GOAL (auto_tac (temp_css addSIs2 [action_mp prem1])) 1,
+	   eres_inst_tac [("F",".~ [.~ B]_f")] InfImpl 1 THEN atac 1,
+	   auto_tac (temp_css addSIs2 [action_mp prem1]),
 	   ALLGOALS (asm_full_simp_tac (simpset() addsimps [square_def,angle_def]))
 	  ]);
 
@@ -904,26 +897,27 @@
 (* ------------------------------------------------------------------------- *)
 section "Well-founded orderings";
 
-qed_goal "wf_dmd" TLA.thy
+val prem1::prems = goal TLA.thy
   "[| (wf r);  \
 \     !!x. sigma |= [](F x .-> <>G .| <>(REX y. #((y,x):r) .& F y))   \
-\  |] ==> sigma |= [](F x .-> <>G)"
-  (fn prem1::prems => 
-         [cut_facts_tac [prem1] 1,
-          etac wf_induct 1,
-          subgoal_tac "sigma |= []((REX y. #((y,x):r) .& F y) .-> <>G)" 1,
-	  cut_facts_tac prems 1,
-	  etac STL4Edup 1, atac 1,
-	  Auto_tac, etac swap 1, atac 1,
-	  rtac dup_dmdD 1,
-	  etac DmdImpl2 1, atac 1,
-	  subgoal_tac "sigma |= [](RALL y. #((y,x):r) .& F y .-> <>G)" 1,
-	  fast_tac (temp_cs addSEs [STL4E]) 1,
-	  auto_tac (temp_css addsimps2 [all_box]),
-	  etac allE 1, etac impCE 1,
-	  rtac (temp_unlift necT) 1,
-	  auto_tac (temp_css addSEs2 [STL4E])
-         ]);
+\  |] ==> sigma |= [](F x .-> <>G)";
+by (cut_facts_tac [prem1] 1);
+by (etac wf_induct 1);
+by (subgoal_tac "sigma |= []((REX y. #((y,x):r) .& F y) .-> <>G)" 1);
+ by (cut_facts_tac prems 1);
+ by (etac STL4Edup 1 THEN atac 1);
+ by (Auto_tac THEN etac swap 1 THEN atac 1);
+ by (rtac dup_dmdD 1);
+ by (etac DmdImpl2 1 THEN atac 1);
+by (subgoal_tac "sigma |= [](RALL y. #((y,x):r) .& F y .-> <>G)" 1);
+ by (fast_tac (temp_cs addSEs [STL4E]) 1);
+by (auto_tac (temp_css addsimps2 [all_box]));
+by (etac allE 1 THEN etac impCE 1);
+ by (rtac (temp_unlift necT) 1);
+by Auto_tac;
+by (auto_tac (temp_css addSEs2 [STL4E]));
+qed "wf_dmd";
+
 
 (* Special case: leadsto via well-foundedness *)
 qed_goalw "wf_leadsto" TLA.thy [leadsto]
@@ -956,17 +950,17 @@
             rewrite_goals_tac more_temp_simps,
             dtac STL2D 1,
             subgoal_tac "sigma |= <>(REX y. #((y, xa) : r) .& ($v .= #y))" 1,
-            SELECT_GOAL (auto_tac (temp_css addsimps2 [DmdAct,Init_def] 
-                                            addEs2 [DmdImplE])) 1,
+            force_tac (temp_css addsimps2 [DmdAct,Init_def] 
+                                            addEs2 [DmdImplE]) 1,
             subgoal_tac "sigma |= (stable ($v .= #xa) .| <>(REX y. #((y, xa) : r) .& $v .= #y)`)" 1,
             case_tac "sigma |= stable ($v .= #xa)" 1,
-            SELECT_GOAL (auto_tac (temp_css addIs2 [temp_mp DmdPrime])) 2,
+            force_tac (temp_css addIs2 [temp_mp DmdPrime]) 2,
             SELECT_GOAL (rewrite_goals_tac ((symmetric (temp_rewrite NotBox))::action_rews)) 1,
             etac swap 1,
             subgoal_tac "sigma |= []($v .= #xa)" 1,
             dres_inst_tac [("P", "$v .= #xa")] (temp_mp BoxPrime) 1,
-            SELECT_GOAL (auto_tac (temp_css addEs2 [STL4E] addsimps2 [square_def])) 1,
-            SELECT_GOAL (auto_tac (temp_css addSIs2 [INV1I] addsimps2 [Init_def])) 1,
+            force_tac (temp_css addEs2 [STL4E] addsimps2 [square_def]) 1,
+            force_tac (temp_css addSIs2 [INV1I] addsimps2 [Init_def]) 1,
             old_auto_tac (temp_css addsimps2 [square_def] addSIs2 [unless] addSEs2 [STL4E])
            ]);
 
@@ -986,7 +980,7 @@
                  dtac (prem RS (temp_mp wf_not_dmd_box_decrease)) 1,
                  dtac BoxDmdDmdBox 1, atac 1,
                  subgoal_tac "sigma |= []<>((#False)::action)" 1,
-                 SELECT_GOAL Auto_tac 1,
+                 Force_tac 1,
                  etac STL4E 1,
                  rtac DmdImpl 1,
                  auto_tac (action_css addsimps2 [square_def] addSEs2 [prem RS wf_irrefl])
@@ -995,17 +989,16 @@
 (* In particular, for natural numbers, if n decreases infinitely often
    then it has to increase infinitely often.
 *)
-qed_goal "nat_box_dmd_decrease" TLA.thy
-  "!!n::nat stfun. []<>(n$ .< $n) .-> []<>($n .< n$)"
-  (fn _ => [Auto_tac,
-            subgoal_tac "sigma |= []<><.~( {[n$,$n]} .: #less_than)>_n" 1,
-            etac thin_rl 1, etac STL4E 1, rtac DmdImpl 1,
-            SELECT_GOAL (auto_tac (claset(), simpset() addsimps [angle_def])) 1,
-            rtac nat_less_cases 1,
-            Auto_tac,
-            rtac (temp_mp wf_box_dmd_decrease) 1,
-            auto_tac (claset() addSEs [STL4E] addSIs [DmdImpl], simpset())
-           ]);
+goal  TLA.thy "!!n::nat stfun. []<>(n$ .< $n) .-> []<>($n .< n$)";
+by Auto_tac;
+by (subgoal_tac "sigma |= []<><.~( {[n$,$n]} .: #less_than)>_n" 1);
+ by (etac thin_rl 1 THEN etac STL4E 1 THEN rtac DmdImpl 1);
+ by (SELECT_GOAL (auto_tac (claset(), simpset() addsimps [angle_def])) 1);
+ by (rtac nat_less_cases 1);
+   by (Auto_tac);
+by (rtac (temp_mp wf_box_dmd_decrease) 1);
+ by (auto_tac (claset() addSEs [STL4E] addSIs [DmdImpl], simpset()));
+qed "nat_box_dmd_decrease";
 
 (* ------------------------------------------------------------------------- *)
 (***           Flexible quantification over state variables                ***)