--- a/src/HOL/MicroJava/BV/BVSpec.thy Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Fri Nov 26 08:46:59 1999 +0100
@@ -52,7 +52,7 @@
in
pc+1 < max_pc \\<and>
is_class G C \\<and>
- (\\<exists>T oT ST'. cfield (G,C) F = Some(C,T) \\<and>
+ (\\<exists>T oT ST'. field (G,C) F = Some(C,T) \\<and>
ST = oT # ST' \\<and>
G \\<turnstile> oT \\<preceq> (Class C) \\<and>
G \\<turnstile> (T # ST' , LT) <=s phi ! (pc+1)))"
@@ -63,7 +63,7 @@
pc+1 < max_pc \\<and>
is_class G C \\<and>
(\\<exists>T vT oT ST'.
- cfield (G,C) F = Some(C,T) \\<and>
+ field (G,C) F = Some(C,T) \\<and>
ST = vT # oT # ST' \\<and>
G \\<turnstile> oT \\<preceq> (Class C) \\<and>
G \\<turnstile> vT \\<preceq> T \\<and>
@@ -155,7 +155,7 @@
(\\<exists>apTs C ST'. ST = (rev apTs) @ (Class C # ST') \\<and>
length apTs = length fpTs \\<and>
(\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
- (\\<exists>D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
+ (\\<exists>D rT b. method (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
G \\<turnstile> (rT # ST' , LT) <=s phi ! (pc+1))))"
consts