| changeset 39246 | 9e58f0499f57 |
| parent 37678 | 0040bafffdef |
| child 40702 | cf26dd7395e4 |
| 39215:7b2631c91a95 | 39246:9e58f0499f57 |
|---|---|
46 of the original one. |
46 of the original one. |
47 *} |
47 *} |
48 |
48 |
49 datatype 'a dual = dual 'a |
49 datatype 'a dual = dual 'a |
50 |
50 |
51 consts |
51 primrec undual :: "'a dual \<Rightarrow> 'a" where |
52 undual :: "'a dual \<Rightarrow> 'a" |
|
53 primrec |
|
54 undual_dual: "undual (dual x) = x" |
52 undual_dual: "undual (dual x) = x" |
55 |
53 |
56 instantiation dual :: (leq) leq |
54 instantiation dual :: (leq) leq |
57 begin |
55 begin |
58 |
56 |