the_inductive_definitions : thm list ref

SYNOPSIS

List of all definitions introduced so far.

DESCRIPTION

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

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.