src/HOL/MicroJava/J/TypeRel.thy
changeset 35416 d8d7d1b785af
parent 33954 1bc3b688548c
child 41589 bbd861837ebc
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -54,9 +54,8 @@
     1.4  apply  auto
     1.5  done
     1.6  
     1.7 -constdefs
     1.8 -  class_rec :: "'c prog \<Rightarrow> cname \<Rightarrow> 'a \<Rightarrow>
     1.9 -    (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.10 +definition class_rec :: "'c prog \<Rightarrow> cname \<Rightarrow> 'a \<Rightarrow>
    1.11 +    (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.12    "class_rec G == wfrec ((subcls1 G)^-1)
    1.13      (\<lambda>r C t f. case class G C of
    1.14           None \<Rightarrow> undefined