changeset 58310 | 91ea607a34d8 |
parent 58249 | 180f1b3508ed |
child 58886 | 8a6cac7c7247 |
--- a/src/HOL/MicroJava/J/Example.thy Thu Sep 11 19:26:59 2014 +0200 +++ b/src/HOL/MicroJava/J/Example.thy Thu Sep 11 19:32:36 2014 +0200 @@ -36,8 +36,8 @@ \end{verbatim} *} -datatype_new cnam' = Base' | Ext' -datatype_new vnam' = vee' | x' | e' +datatype cnam' = Base' | Ext' +datatype vnam' = vee' | x' | e' text {* @{text cnam'} and @{text vnam'} are intended to be isomorphic