changeset 11299 | 1d3d110c456e |
parent 11298 | acd83fa66e92 |
child 11549 | e7265e70fd7c |
--- a/src/HOL/MicroJava/BV/Kildall.thy Mon May 14 09:58:22 2001 +0200 +++ b/src/HOL/MicroJava/BV/Kildall.thy Wed May 16 12:31:25 2001 +0200 @@ -349,7 +349,7 @@ pres_type step n A; bounded succs n; mono r step n A |] ==> is_bcv r T step succs n A (kildall r f step succs)" -apply(unfold is_bcv_def welltyping_def) +apply(unfold is_bcv_def wt_step_def) apply(insert kildall_properties[of A]) apply(simp add:stables_def) apply clarify