1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
\DOC the_inductive_definitions
\TYPE {the_inductive_definitions : thm list ref}
\SYNOPSIS
List of all definitions introduced so far.
\DESCRIBE
The reference variable {the_inductive_definitions} holds the list of
inductive definitions made so far using {new_inductive_definition}, which
automatically augments it.
\FAILURE
Not applicable.
\EXAMPLE
If we examine the list in HOL Light's initial state, we see the most recent
inductive definition is finiteness of a set:
{
# !the_inductive_definitions;;
val it : (thm * thm * thm) list =
[(|- FINITE {} /\ (!x s. FINITE s ==> FINITE (x INSERT s)),
|- !FINITE'. FINITE' {} /\ (!x s. FINITE' s ==> FINITE' (x INSERT s))
==> (!a. FINITE a ==> FINITE' a),
|- !a. FINITE a <=> a = {} \/ (?x s. a = x INSERT s /\ FINITE s));
...
...]
}
\USES
This list is not logically necessary and is not part of HOL Light's logical
core, but it is used outside the core so that multiple instances of the same
inductive definition are quietly ``ignored'' rather than rejected.
Users may also sometimes find it convenient.
\SEEALSO
axioms, constants, define, definitions, new_definition,
new_inductive_definition, new_recursive_definition, new_specification,
the_definitions, the_specifications.
\ENDDOC
|
