--- a/src/HOLCF/IOA/meta_theory/LiveIOA.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.ML Fri Jan 29 16:23:56 1999 +0100
@@ -10,7 +10,7 @@
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";
@@ -24,7 +24,7 @@
(* ---------------------------------------------------------------- *)
-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)";