equal
deleted
inserted
replaced
1 open Example; |
|
2 |
1 |
3 AddIs [widen.null]; |
2 AddIs [widen.null]; |
4 |
3 |
5 Addsimps [inj_cnam_, inj_vnam_]; |
4 Addsimps [inj_cnam_, inj_vnam_]; |
6 Addsimps [Base_not_Object,Ext_not_Object]; |
5 Addsimps [Base_not_Object,Ext_not_Object]; |
128 br method_rec_ 1; |
127 br method_rec_ 1; |
129 by Auto_tac; |
128 by Auto_tac; |
130 qed "method_Base"; |
129 qed "method_Base"; |
131 Addsimps [method_Base]; |
130 Addsimps [method_Base]; |
132 |
131 |
133 Goal "method (tprg, Ext) = (method (tprg, Base) \\<oplus> map_of \ |
132 Goal "method (tprg, Ext) = (method (tprg, Base) ++ map_of \ |
134 \ [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])"; |
133 \ [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])"; |
135 br trans 1; |
134 br trans 1; |
136 br method_rec_ 1; |
135 br method_rec_ 1; |
137 by Auto_tac; |
136 by Auto_tac; |
138 qed "method_Ext"; |
137 qed "method_Ext"; |