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