the_inductive_definitions : thm list ref
# !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)); ... ...]