| author | wenzelm |
| Fri, 06 Oct 2000 17:35:58 +0200 | |
| changeset 10168 | 50be659d4222 |
| parent 9802 | adda1dc18bb8 |
| permissions | -rw-r--r-- |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
1 |
|
| 7721 | 2 |
val accI = thm "acc.accI"; |
| 9802 | 3 |
val acc_induct = thm "acc_induct"; |
4 |
val acc_downward = thm "acc_downward"; |
|
5 |
val acc_downwards = thm "acc_downwards"; |
|
6 |
val acc_wfI = thm "acc_wfI"; |
|
7 |
val acc_wfD = thm "acc_wfD"; |
|
8 |
val wf_acc_iff = thm "wf_acc_iff"; |