src/HOL/NanoJava/TypeRel.thy
changeset 12264 9c356e2da72f
parent 11626 0dbfb578bf75
child 13867 1fdecd15437f
     1.1 --- a/src/HOL/NanoJava/TypeRel.thy	Wed Nov 21 20:20:18 2001 +0100
     1.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Thu Nov 22 17:12:08 2001 +0100
     1.3 @@ -133,10 +133,10 @@
     1.4  
     1.5  
     1.6  --{* Fields of a class, with inheritance and hiding *}
     1.7 -defs field_def: "field C \<equiv> class_rec C fields"
     1.8 +defs field_def: "field C \<equiv> class_rec C flds"
     1.9  
    1.10 -lemma fields_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
    1.11 -field C = (if C=Object then empty else field (super m)) ++ map_of (fields m)"
    1.12 +lemma flds_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
    1.13 +field C = (if C=Object then empty else field (super m)) ++ map_of (flds m)"
    1.14  apply (unfold field_def)
    1.15  apply (erule (1) class_rec [THEN trans]);
    1.16  apply simp