IMP_CANON : (thm -> thm list)
STRUCTURE
SYNOPSIS
Puts theorem into a ‘canonical’ form.
DESCRIPTION
IMP_CANON puts a theorem in ‘canonical’ form by removing quantifiers and breaking apart conjunctions, as well as disjunctions which form the antecedent of implications. It applies the following transformation rules:
      A |- t1 /\ t2           A |- !x. t           A |- (t1 /\ t2) ==> t
   -------------------       ------------         ------------------------
    A |- t1   A |- t2           A |- t             A |- t1 ==> (t2 ==> t)

        A |- (t1 \/ t2) ==> t              A |- (?x. t1) ==> t2
   -------------------------------        ----------------------
    A |- t1 ==> t   A |- t2 ==> t          A |- t1[x'/x] ==> t2

FAILURE
Never fails, but if there is no scope for one of the above reductions, merely gives a list whose only member is the original theorem.
COMMENTS
This is a rather ad-hoc inference rule, and its use is not recommended.
SEEALSO
HOL  Trindemossen-1