| changeset 45605 | a89b4bc311a5 |
| parent 42793 | 88bee9f6eec7 |
| child 45827 | 66c68453455c |
| 45604:29cf40fe8daf | 45605:a89b4bc311a5 |
|---|---|
194 apply (drule AxSem.Impl) |
194 apply (drule AxSem.Impl) |
195 apply (erule Weaken) |
195 apply (erule Weaken) |
196 apply (auto del: image_eqI intro: rev_image_eqI) |
196 apply (auto del: image_eqI intro: rev_image_eqI) |
197 done |
197 done |
198 |
198 |
199 lemmas Impl1 = AxSem.Impl [of _ _ _ "{Cm}", simplified, standard] |
199 lemmas Impl1 = AxSem.Impl [of _ _ _ "{Cm}", simplified] for Cm |
200 |
200 |
201 end |
201 end |