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).
structure Main =
struct
val thy = the_context ();
end;
simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);