changeset 12951 | a9fdcb71d252 |
parent 12911 | 704713ca07ea |
child 13006 | 51c5f3f11d16 |
--- a/src/HOL/MicroJava/BV/EffectMono.thy Tue Feb 26 13:47:19 2002 +0100 +++ b/src/HOL/MicroJava/BV/EffectMono.thy Tue Feb 26 15:45:32 2002 +0100 @@ -151,7 +151,7 @@ "is_class G cname" and oT: "G\<turnstile> oT\<preceq> (Class cname)" and vT: "G\<turnstile> vT\<preceq> b" and - xc: "is_class G (Xcpt NullPointer)" + xc: "Ball (set (match G (Xcpt NullPointer) pc et)) (is_class G)" by force moreover from s1 G