equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 section \<open>Miscellaneous Polymorphic Examples\<close> |
9 section \<open>Miscellaneous Polymorphic Examples\<close> |
10 |
10 |
11 theory Misc_Poly |
11 theory Misc_Poly |
12 imports "~~/src/HOL/Library/BNF_Corec" |
12 imports "HOL-Library.BNF_Corec" |
13 begin |
13 begin |
14 |
14 |
15 codatatype ('a, 'b) T0 = |
15 codatatype ('a, 'b) T0 = |
16 C1 (lab: "'a * 'b") (tl11: "('a, 'b) T0") (tl12: "('a, 'b) T0") |
16 C1 (lab: "'a * 'b") (tl11: "('a, 'b) T0") (tl12: "('a, 'b) T0") |
17 | C2 (lab: "'a * 'b") (tl2: "('a, 'b) T0") |
17 | C2 (lab: "'a * 'b") (tl2: "('a, 'b) T0") |