HOL/equalities: added some identities from ZF/equalities
HOL/equalities/constant_UN: renamed UN1_constant
HOL/equalities/Union_Un_distrib: deleted duplicate!
HOL/equalities/Union_Int_subset: new
let
fun tac ss = resolve_tac(prems_of_ss ss) ORELSE' asm_simp_tac ss;
val ss = set_prove_tac(HOL_ss addsimps [Suc_lessD],tac)
in prove_goal Nat.thy "!!x. Suc(Suc(Suc(x)))<y ==> x<y"
(fn _ => [asm_simp_tac ss 1])
end;