renamed "fields" to "flds" (avoid clash with new "fields" operation);
authorwenzelm
Thu, 22 Nov 2001 17:12:08 +0100
changeset 12264 9c356e2da72f
parent 12263 6f2acf10e2a2
child 12265 6df58e87ec91
renamed "fields" to "flds" (avoid clash with new "fields" operation);
src/HOL/NanoJava/Decl.thy
src/HOL/NanoJava/TypeRel.thy
--- a/src/HOL/NanoJava/Decl.thy	Wed Nov 21 20:20:18 2001 +0100
+++ b/src/HOL/NanoJava/Decl.thy	Thu Nov 22 17:12:08 2001 +0100
@@ -28,7 +28,7 @@
 
 record	class
 	= super   :: cname
-          fields  ::"fdecl list"
+          flds    ::"fdecl list"
           methods ::"mdecl list"
 
 text{* Class declaration *}
--- a/src/HOL/NanoJava/TypeRel.thy	Wed Nov 21 20:20:18 2001 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy	Thu Nov 22 17:12:08 2001 +0100
@@ -133,10 +133,10 @@
 
 
 --{* Fields of a class, with inheritance and hiding *}
-defs field_def: "field C \<equiv> class_rec C fields"
+defs field_def: "field C \<equiv> class_rec C flds"
 
-lemma fields_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
-field C = (if C=Object then empty else field (super m)) ++ map_of (fields m)"
+lemma flds_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
+field C = (if C=Object then empty else field (super m)) ++ map_of (flds m)"
 apply (unfold field_def)
 apply (erule (1) class_rec [THEN trans]);
 apply simp