| changeset 45605 | a89b4bc311a5 |
| parent 42793 | 88bee9f6eec7 |
| child 45827 | 66c68453455c |
--- a/src/HOL/NanoJava/AxSem.thy Sun Nov 20 20:59:30 2011 +0100 +++ b/src/HOL/NanoJava/AxSem.thy Sun Nov 20 21:05:23 2011 +0100 @@ -196,6 +196,6 @@ apply (auto del: image_eqI intro: rev_image_eqI) done -lemmas Impl1 = AxSem.Impl [of _ _ _ "{Cm}", simplified, standard] +lemmas Impl1 = AxSem.Impl [of _ _ _ "{Cm}", simplified] for Cm end