equal
deleted
inserted
replaced
7 |
7 |
8 See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. |
8 See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. |
9 Research Report 92-49, LIP, ENS Lyon. Dec 1992. |
9 Research Report 92-49, LIP, ENS Lyon. Dec 1992. |
10 *) |
10 *) |
11 |
11 |
12 Acc = WF + |
12 Acc = WF + Inductive + |
13 |
13 |
14 constdefs |
14 constdefs |
15 pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*) |
15 pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*) |
16 "pred x r == {y. (y,x):r}" |
16 "pred x r == {y. (y,x):r}" |
17 |
17 |