equal
deleted
inserted
replaced
5 |
5 |
6 Disjoint sums in Zermelo-Fraenkel Set Theory |
6 Disjoint sums in Zermelo-Fraenkel Set Theory |
7 "Part" primitive for simultaneous recursive type definitions |
7 "Part" primitive for simultaneous recursive type definitions |
8 *) |
8 *) |
9 |
9 |
10 Sum = Bool + |
10 Sum = Bool + "simpdata" + |
11 consts |
11 consts |
12 "+" :: "[i,i]=>i" (infixr 65) |
12 "+" :: "[i,i]=>i" (infixr 65) |
13 Inl,Inr :: "i=>i" |
13 Inl,Inr :: "i=>i" |
14 case :: "[i=>i, i=>i, i]=>i" |
14 case :: "[i=>i, i=>i, i]=>i" |
15 Part :: "[i,i=>i] => i" |
15 Part :: "[i,i=>i] => i" |