changeset 809 | 1daa0269eb5d |
parent 578 | efc648d29dd0 |
child 1401 | 0c439768f45c |
808:c51c1f59e59e | 809:1daa0269eb5d |
---|---|
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 + "Inductive" + |
12 Acc = WF + Inductive + |
13 |
13 |
14 consts |
14 consts |
15 acc :: "i=>i" |
15 acc :: "i=>i" |
16 |
16 |
17 inductive |
17 inductive |