minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections;
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;