changeset 5143 | b94cd208f073 |
parent 5132 | 24f992a25adc |
child 5148 | 74919e8f221c |
--- 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);