equal
deleted
inserted
replaced
1 (* Title: CCL/Lazy/fix.thy |
1 (* Title: CCL/Lazy/fix.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Martin Coen |
3 Author: Martin Coen |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Tentative attempt at including fixed point induction. |
6 Tentative attempt at including fixed point induction. |
7 Justified by Smith. |
7 Justified by Smith. |
8 *) |
8 *) |
9 |
9 |
10 Fix = Type + |
10 Fix = Type + |
11 |
11 |
12 consts |
12 consts |
13 |
13 |
14 idgen :: "[i]=>i" |
14 idgen :: "[i]=>i" |
15 INCL :: "[i=>o]=>o" |
15 INCL :: "[i=>o]=>o" |
16 |
16 |
17 rules |
17 rules |
18 |
18 |
19 idgen_def |
19 idgen_def |