README
1+ ===================================================================== +
2| |
3| LIBRARY : IndDefLib |
4| |
5| DESCRIPTION : Inductive definitions package. |
6| |
7| AUTHOR : J.R.Harrison, T.F. Melham |
8| DATE : 1996 |
9| |
10| PORTED BY : D.R.Syme |
11| DATE : 1996 |
12| |
13| MODIFIED : R.J.Boulton |
14| DATE : 6 August 1996 |
15| |
16| MODIFIED : K. Slind |
17| DATE : Jan. 02. 2000 |
18+ ===================================================================== +
19
20Inductive definitions package.
21See the following paper:
22
23 J. Harrison
24 "Inductive Definitions: Automation and Application"
25 In: E. T. Schubert, P. J. Windley and J. Alves-Foss (editors),
26 "Proceedings of the 8th International Workshop on Higher Order Logic
27 Theorem Proving and Its Applications", Aspen Grove, UT, USA, September 1995.
28 Volume 971 of Lecture Notes in Computer Science, Springer-Verlag,
29 pages 200-213.
30
31Relevant structures: IndDefLib
32
33Functions:
34 "new_inductive_definition" and functions in IndDefRules.
35
36