NameDateSize

..25-Jul-201970

CoIndDefLib.sigH A D25-Jul-2019714

CoIndDefLib.smlH A D25-Jul-20198.4 KiB

HolmakefileH A D25-Jul-2019115

IndDefLib.sigH A D25-Jul-2019991

IndDefLib.smlH A D25-Jul-20196.4 KiB

IndDefRules.sigH A D25-Jul-2019267

IndDefRules.smlH A D25-Jul-201926.6 KiB

InductiveDefinition.sigH A D25-Jul-20191.5 KiB

InductiveDefinition.smlH A D25-Jul-201936.7 KiB

Manual/H25-Jul-20196

READMEH A D25-Jul-20191.1 KiB

selftest.smlH A D25-Jul-20193.6 KiB

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