| changeset 124 | 858ab9a9b047 |
| parent 0 | a5a9c433f639 |
| 123:0a2f744e008a | 124:858ab9a9b047 |
|---|---|
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Epsilon induction and recursion |
6 Epsilon induction and recursion |
7 *) |
7 *) |
8 |
8 |
9 Epsilon = Nat + |
9 Epsilon = Nat + "mono" + |
10 consts |
10 consts |
11 eclose,rank :: "i=>i" |
11 eclose,rank :: "i=>i" |
12 transrec :: "[i, [i,i]=>i] =>i" |
12 transrec :: "[i, [i,i]=>i] =>i" |
13 |
13 |
14 rules |
14 rules |