src/HOL/Bali/DeclConcepts.thy
changeset 30235 58d147683393
parent 25143 2a1acc88a180
child 32134 ee143615019c
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Tue Mar 03 17:05:18 2009 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Wed Mar 04 10:47:20 2009 +0100
     1.3 @@ -1385,7 +1385,7 @@
     1.4  "imethds G I 
     1.5    \<equiv> iface_rec (G,I)  
     1.6                (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
     1.7 -                        (o2s \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
     1.8 +                        (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
     1.9  text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
    1.10  
    1.11  constdefs
    1.12 @@ -1528,7 +1528,7 @@
    1.13  
    1.14  lemma imethds_rec: "\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow>  
    1.15    imethds G I = Un_tables ((\<lambda>J. imethds  G J)`set (isuperIfs i)) \<oplus>\<oplus>  
    1.16 -                      (o2s \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))"
    1.17 +                      (Option.set \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))"
    1.18  apply (unfold imethds_def)
    1.19  apply (rule iface_rec [THEN trans])
    1.20  apply auto