src/HOL/Bali/DeclConcepts.thy
changeset 35440 bdf8ad377877
parent 35416 d8d7d1b785af
child 35547 991a6af75978
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Mon Mar 01 18:49:55 2010 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Tue Mar 02 12:26:50 2010 +0100
     1.3 @@ -1381,7 +1381,7 @@
     1.4  
     1.5  definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
     1.6  "imethds G I 
     1.7 -  \<equiv> iface_rec (G,I)  
     1.8 +  \<equiv> iface_rec G I  
     1.9                (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
    1.10                          (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
    1.11  text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
    1.12 @@ -1396,7 +1396,7 @@
    1.13  definition methd :: "prog \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
    1.14  
    1.15  "methd G C 
    1.16 - \<equiv> class_rec (G,C) empty
    1.17 + \<equiv> class_rec G C empty
    1.18               (\<lambda>C c subcls_mthds. 
    1.19                 filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)
    1.20                            subcls_mthds 
    1.21 @@ -1429,7 +1429,7 @@
    1.22          then (case methd G statC sig of
    1.23                  None \<Rightarrow> None
    1.24                | Some statM 
    1.25 -                  \<Rightarrow> (class_rec (G,dynC) empty
    1.26 +                  \<Rightarrow> (class_rec G dynC empty
    1.27                         (\<lambda>C c subcls_mthds. 
    1.28                            subcls_mthds
    1.29                            ++
    1.30 @@ -1481,7 +1481,7 @@
    1.31  
    1.32  definition fields :: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list" where
    1.33  "fields G C 
    1.34 -  \<equiv> class_rec (G,C) [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
    1.35 +  \<equiv> class_rec G C [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
    1.36  text {* @{term "fields G C"} 
    1.37       list of fields of a class, including all the fields of the superclasses
    1.38       (private, inherited and hidden ones) not only the accessible ones
    1.39 @@ -1805,7 +1805,7 @@
    1.40                  (\<lambda>_ dynM. G,sig \<turnstile> dynM overrides statM \<or> dynM = statM)
    1.41                  (methd G C)"
    1.42          let "?class_rec C" =
    1.43 -              "(class_rec (G, C) empty
    1.44 +              "(class_rec G C empty
    1.45                             (\<lambda>C c subcls_mthds. subcls_mthds ++ (?filter C)))"
    1.46          from statM Subcls ws subclseq_dynC_statC
    1.47          have dynmethd_dynC_def:
    1.48 @@ -2270,7 +2270,7 @@
    1.49  section "calculation of the superclasses of a class"
    1.50  
    1.51  definition superclasses :: "prog \<Rightarrow> qtname \<Rightarrow> qtname set" where
    1.52 - "superclasses G C \<equiv> class_rec (G,C) {} 
    1.53 + "superclasses G C \<equiv> class_rec G C {} 
    1.54                         (\<lambda> C c superclss. (if C=Object 
    1.55                                              then {} 
    1.56                                              else insert (super c) superclss))"