changeset 10138 | 412a3ced6efd |
parent 10042 | 7164dc0d24d8 |
child 10613 | 78b1d6c3ee9c |
--- a/src/HOL/MicroJava/J/Example.ML Tue Oct 03 18:40:25 2000 +0200 +++ b/src/HOL/MicroJava/J/Example.ML Tue Oct 03 18:44:19 2000 +0200 @@ -1,4 +1,3 @@ -open Example; AddIs [widen.null]; @@ -130,7 +129,7 @@ qed "method_Base"; Addsimps [method_Base]; -Goal "method (tprg, Ext) = (method (tprg, Base) \\<oplus> map_of \ +Goal "method (tprg, Ext) = (method (tprg, Base) ++ map_of \ \ [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])"; br trans 1; br method_rec_ 1;