--- a/src/HOL/Lex/RegSet_of_nat_DA.ML Tue May 02 18:42:48 2000 +0200
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML Tue May 02 18:44:33 2000 +0200
@@ -130,9 +130,8 @@
qed_spec_mp "deltas_concat";
Addsimps [deltas_concat];
-goal Arith.thy "!!n. [| n < Suc k; n ~= k |] ==> n < k";
-by (etac linorder_neqE 1);
-by (ALLGOALS Simp_tac);
+Goal "[| n < Suc k; n ~= k |] ==> n < k";
+by (arith_tac 1);
val lemma = result();
Goal
--- a/src/HOL/UNITY/Lift.ML Tue May 02 18:42:48 2000 +0200
+++ b/src/HOL/UNITY/Lift.ML Tue May 02 18:44:33 2000 +0200
@@ -244,8 +244,7 @@
i.e. the trivial disjunction, leading to an asymmetrical proof.*)
Goal "#0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
by (asm_simp_tac metric_ss 1);
-by (force_tac (claset() delrules [impCE] addEs [impCE],
- simpset() addsimps conj_comms) 1);
+by (Force_tac 1);
qed "E_thm16c";