test.ML

added Pair_eq to pair_ss in prod.ML

removed it locally in llist.ML because preconditions of the form <a,b> =
<?x,?y>, which used to be solved by reflexivity, now rewrote to a = ?x & b =
?y, which is not solved by reflexivity.

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;