| changeset 58249 | 180f1b3508ed |
| parent 54711 | 15a642b9ffac |
| child 58310 | 91ea607a34d8 |
| 58248:25af24e1f37b | 58249:180f1b3508ed |
|---|---|
18 Fin(H)"} |
18 Fin(H)"} |
19 *} |
19 *} |
20 |
20 |
21 subsection {* The datatype of propositions *} |
21 subsection {* The datatype of propositions *} |
22 |
22 |
23 datatype 'a pl = |
23 datatype_new 'a pl = |
24 false | |
24 false | |
25 var 'a ("#_" [1000]) | |
25 var 'a ("#_" [1000]) | |
26 imp "'a pl" "'a pl" (infixr "->" 90) |
26 imp "'a pl" "'a pl" (infixr "->" 90) |
27 |
27 |
28 |
28 |