Added "using" to the beginning of original newman proof again, because
it was lost during last update; renamed second version of newman to
newman' (this allows for a comparison of the primitive proof objects,
for example).
(*Dummy theory to document dependencies *)
fin = Arith + "inductive" + "constructor" + "intr_elim" + "equalities"