src/HOL/UNITY/WFair.ML

 
 Weak Fairness versions of transient, ensures, leadsTo.
 
 From Misra, "A Logic for Concurrent Programming", 1994
 *)
-
-open WFair;
-
-Goal "Union(B) Int A = Union((%C. C Int A)``B)";
-by (Blast_tac 1);
-qed "Int_Union_Union";
 
 
 (*** transient ***)
 
 Goalw [stable_def, constrains_def, transient_def]

 \     !!A B. ensures Acts A B ==> P A B; \
 \     !!A B C. [| leadsTo Acts A B; P A B; leadsTo Acts B C; P B C |] \
 \              ==> P A C; \
 \     !!B S. ALL A:S. leadsTo Acts A B & P A B ==> P (Union S) B \
 \  |] ==> P za zb";
-br (major RS leadsto.induct) 1;
+by (rtac (major RS leadsto.induct) 1);
 by (REPEAT (blast_tac (claset() addIs prems) 1));
 qed "leadsTo_induct";
 
 
 Goal "[| A<=B;  id: Acts |] ==> leadsTo Acts A B";