src/HOL/TLA/Inc/Inc.thy

   by (auto elim!: Stable squareE simp: Psi_defs)
 
 lemma N1_enabled_at_g: "|- pc1 = #g --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
   apply clarsimp
   apply (rule_tac F = gamma1 in enabled_mono)
-   apply (tactic {* enabled_tac (thm "Inc_base") 1 *})
+   apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
   apply (force simp: gamma1_def)
   apply (force simp: angle_def gamma1_def N1_def)
   done
 
 lemma g1_leadsto_a1:

 
 (* symmetrical for N2, and similar for beta2 *)
 lemma N2_enabled_at_g: "|- pc2 = #g --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
   apply clarsimp
   apply (rule_tac F = gamma2 in enabled_mono)
-  apply (tactic {* enabled_tac (thm "Inc_base") 1 *})
+  apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
    apply (force simp: gamma2_def)
   apply (force simp: angle_def gamma2_def N2_def)
   done
 
 lemma g2_leadsto_a2:

   done
 
 lemma N2_enabled_at_b: "|- pc2 = #b --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
   apply clarsimp
   apply (rule_tac F = beta2 in enabled_mono)
-   apply (tactic {* enabled_tac (thm "Inc_base") 1 *})
+   apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
    apply (force simp: beta2_def)
   apply (force simp: angle_def beta2_def N2_def)
   done
 
 lemma b2_leadsto_g2:

 
 lemma N1_enabled_at_both_a:
   "|- pc2 = #a & (PsiInv & pc1 = #a) --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
   apply clarsimp
   apply (rule_tac F = alpha1 in enabled_mono)
-  apply (tactic {* enabled_tac (thm "Inc_base") 1 *})
+  apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
    apply (force simp: alpha1_def PsiInv_defs)
   apply (force simp: angle_def alpha1_def N1_def)
   done
 
 lemma a1_leadsto_b1:

   done
 
 lemma N1_enabled_at_b: "|- pc1 = #b --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
   apply clarsimp
   apply (rule_tac F = beta1 in enabled_mono)
-   apply (tactic {* enabled_tac (thm "Inc_base") 1 *})
+   apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
    apply (force simp: beta1_def)
   apply (force simp: angle_def beta1_def N1_def)
   done
 
 (* Now assemble the bits and pieces to prove that Psi is fair. *)