src/HOLCF/IOA/meta_theory/LiveIOA.ML

 
 *)   
 
 Delsimps [split_paired_Ex];
 
-goalw thy [live_implements_def] 
+Goalw [live_implements_def] 
 "!! A. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] \
 \     ==> live_implements (A,LA) (C,LC)"; 
 auto();
 qed"live_implements_trans";
 

 (* ---------------------------------------------------------------- *)
 (*                Correctness of live refmap                        *)
 (* ---------------------------------------------------------------- *)
 
 
-goal thy "!! f. [| inp(C)=inp(A); out(C)=out(A); \
+Goal "!! f. [| inp(C)=inp(A); out(C)=out(A); \
 \                  is_live_ref_map f (C,M) (A,L) |] \
 \               ==> live_implements (C,M) (A,L)";
 
 by (asm_full_simp_tac (simpset() addsimps [is_live_ref_map_def, live_implements_def,
 livetraces_def,liveexecutions_def]) 1);

 
 (*
 
 (* Classical Fairness and Fairness by Temporal Formula coincide *)
  
-goal thy "!! ex. Finite (snd ex) ==> \
+Goal "!! ex. Finite (snd ex) ==> \
 \          (ex |== WF A acts) = (~ Enabled A acts (laststate ex))";
 
 In 3 steps:
 
 1) []<>P and <>[]P mean both P (Last`s)