equal
deleted
inserted
replaced
92 nitpick [show_datatypes, expect = genuine] |
92 nitpick [show_datatypes, expect = genuine] |
93 oops |
93 oops |
94 |
94 |
95 subsection {* 2.7. Typedefs, Records, Rationals, and Reals *} |
95 subsection {* 2.7. Typedefs, Records, Rationals, and Reals *} |
96 |
96 |
97 typedef three = "{0\<Colon>nat, 1, 2}" |
97 definition "three = {0\<Colon>nat, 1, 2}" |
98 by blast |
98 typedef (open) three = three |
|
99 unfolding three_def by blast |
99 |
100 |
100 definition A :: three where "A \<equiv> Abs_three 0" |
101 definition A :: three where "A \<equiv> Abs_three 0" |
101 definition B :: three where "B \<equiv> Abs_three 1" |
102 definition B :: three where "B \<equiv> Abs_three 1" |
102 definition C :: three where "C \<equiv> Abs_three 2" |
103 definition C :: three where "C \<equiv> Abs_three 2" |
103 |
104 |