changeset 58249 | 180f1b3508ed |
parent 58042 | ffa9e39763e3 |
child 58310 | 91ea607a34d8 |
--- a/src/HOL/Library/Extended_Real.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Library/Extended_Real.thy Tue Sep 09 20:51:36 2014 +0200 @@ -20,7 +20,7 @@ subsection {* Definition and basic properties *} -datatype ereal = ereal real | PInfty | MInfty +datatype_new ereal = ereal real | PInfty | MInfty instantiation ereal :: uminus begin