beautified "match"
authorkleing
Sat Nov 16 23:01:59 2002 +0100 (2002-11-16)
changeset 137189f94248d2f5a
parent 13717 78f91fcdf560
child 13719 44fed7d0c305
beautified "match"
src/HOL/MicroJava/BV/EffectMono.thy
     1.1 --- a/src/HOL/MicroJava/BV/EffectMono.thy	Sat Nov 16 22:54:39 2002 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/EffectMono.thy	Sat Nov 16 23:01:59 2002 +0100
     1.3 @@ -151,7 +151,7 @@
     1.4                    "is_class G cname" and
     1.5                oT: "G\<turnstile> oT\<preceq> (Class cname)" and
     1.6                vT: "G\<turnstile> vT\<preceq> b" and
     1.7 -              xc: "Ball (set (match G (Xcpt NullPointer) pc et)) (is_class G)"
     1.8 +              xc: "Ball (set (match G NullPointer pc et)) (is_class G)"
     1.9          by force
    1.10        moreover
    1.11        from s1 G