| changeset 53591 | b6e2993fd0d3 |
| parent 53588 | 11a77e4aa98b |
| child 54193 | bc07627c5dcd |
--- a/src/HOL/BNF/Examples/Misc_Codatatype.thy Fri Sep 13 00:55:44 2013 +0200 +++ b/src/HOL/BNF/Examples/Misc_Codatatype.thy Fri Sep 13 02:26:59 2013 +0200 @@ -43,6 +43,8 @@ ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 *) +codatatype 'a p = P "'a + 'a p" + codatatype 'a J1 = J11 'a "'a J1" | J12 'a "'a J2" and 'a J2 = J21 | J22 "'a J1" "'a J2"