the_inductive_definitions : thm list ref
List of all definitions introduced so far.
The reference variable the_inductive_definitions holds the list of
inductive definitions made so far using new_inductive_definition, which
automatically augments it.
- FAILURE CONDITIONS
If we examine the list in HOL Light's initial state, we see the most recent
inductive definition is finiteness of a set:
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));
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.
- SEE ALSO
axioms, constants, define, definitions, new_definition,
new_inductive_definition, new_recursive_definition, new_specification,