Modified proofs for new hyp_subst_tac.

--- a/src/ZF/ex/Integ.ML	Thu Apr 06 12:22:26 1995 +0200
+++ b/src/ZF/ex/Integ.ML	Thu Apr 06 12:24:56 1995 +0200
@@ -133,10 +133,13 @@
 
 (**** znegative: the test for negative integers ****)
 
+(*No natural number is negative!*)
 goalw Integ.thy [znegative_def, znat_def]  "~ znegative($# n)";
-by (asm_full_simp_tac (intrel_ss setloop K(safe_tac intrel_cs)) 1);
-by (etac rev_mp 1);
-by (asm_simp_tac (arith_ss addsimps [add_le_self2 RS le_imp_not_lt]) 1);
+by (safe_tac intrel_cs);
+by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
+by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
+by (fast_tac (FOL_cs addss
+	      (intrel_ss addsimps [add_le_self2 RS le_imp_not_lt])) 1);
 qed "not_znegative_znat";
 
 goalw Integ.thy [znegative_def, znat_def]