src/HOLCF/IOA/meta_theory/LiveIOA.ML

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

 (* ---------------------------------------------------------------- *)
 (*                Correctness of live refmap                        *)
 (* ---------------------------------------------------------------- *)
 
 
-Goal "!! f. [| inp(C)=inp(A); out(C)=out(A); \
+Goal "[| 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);