intro_tacsf: replaced ORELSE by APPEND in order to stop
errors that arise when unconstrained equalities appear in the premises. Could
cause runtimes to increase...
(*Dummy theory to document dependencies *)
fin = Arith + "inductive" + "constructor" + "intr_elim" + "equalities"