src/HOL/UNITY/SubstAx.thy
changeset 19769 c40ce2de2020
parent 16417 9bc16273c2d4
child 35355 613e133966ea
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/UNITY/SubstAx.thy	Sun Jun 04 10:52:47 2006 +0200
     1.2 +++ b/src/HOL/UNITY/SubstAx.thy	Mon Jun 05 14:22:58 2006 +0200
     1.3 @@ -363,7 +363,7 @@
     1.4        ==> F \<in> A LeadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)"
     1.5  apply (rule_tac f = f and f1 = "%k. l - k" 
     1.6         in wf_less_than [THEN wf_inv_image, THEN LeadsTo_wf_induct])
     1.7 -apply (simp add: inv_image_def Image_singleton, clarify)
     1.8 +apply (simp add: Image_singleton, clarify)
     1.9  apply (case_tac "m<l")
    1.10   apply (blast intro: LeadsTo_weaken_R diff_less_mono2)
    1.11  apply (blast intro: not_leE subset_imp_LeadsTo)