src/HOL/MicroJava/J/TypeRel.thy
changeset 28524 644b62cf678f
parent 23757 087b0a241557
child 28562 4e74209f113e
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Oct 07 16:07:40 2008 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Oct 07 16:07:50 2008 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4      (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
     1.5    "class_rec G == wfrec {(C, D). (subcls1 G)^--1 C D}
     1.6      (\<lambda>r C t f. case class G C of
     1.7 -         None \<Rightarrow> arbitrary
     1.8 +         None \<Rightarrow> undefined
     1.9         | Some (D,fs,ms) \<Rightarrow> 
    1.10             f C fs ms (if C = Object then t else r D t f))"
    1.11  
    1.12 @@ -68,10 +68,10 @@
    1.13  definition
    1.14    "wf_class G = wfP ((subcls1 G)^--1)"
    1.15  
    1.16 -lemma class_rec_func [code func]:
    1.17 +lemma class_rec_func (*[code func]*):
    1.18    "class_rec G C t f = (if wf_class G then
    1.19      (case class G C
    1.20 -      of None \<Rightarrow> arbitrary
    1.21 +      of None \<Rightarrow> undefined
    1.22         | Some (D, fs, ms) \<Rightarrow> f C fs ms (if C = Object then t else class_rec G D t f))
    1.23      else class_rec G C t f)"
    1.24  proof (cases "wf_class G")