src/HOL/Bali/Example.thy
changeset 30235 58d147683393
parent 28524 644b62cf678f
child 31166 a90fe83f58ea
     1.1 --- a/src/HOL/Bali/Example.thy	Tue Mar 03 17:05:18 2009 +0100
     1.2 +++ b/src/HOL/Bali/Example.thy	Wed Mar 04 10:47:20 2009 +0100
     1.3 @@ -458,7 +458,7 @@
     1.4  lemmas methd_rec'  = methd_rec  [OF _ ws_tprg]
     1.5  
     1.6  lemma imethds_HasFoo [simp]: 
     1.7 -  "imethds tprg HasFoo = o2s \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
     1.8 +  "imethds tprg HasFoo = Option.set \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
     1.9  apply (rule trans)
    1.10  apply (rule imethds_rec')
    1.11  apply  (auto simp add: HasFooInt_def)