src/HOL/IOA/IOA.ML

--- a/src/HOL/IOA/IOA.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/IOA/IOA.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -46,7 +46,7 @@
   by (Fast_tac 1);
 qed "mk_trace_thm";
 
-Goalw [reachable_def] "!!A. s:starts_of(A) ==> reachable A s";
+Goalw [reachable_def] "s:starts_of(A) ==> reachable A s";
   by (res_inst_tac [("x","(%i. None,%i. s)")] bexI 1);
   by (Simp_tac 1);
   by (asm_simp_tac (simpset() addsimps exec_rws) 1);