# HG changeset patch
# User paulson
# Date 957285873 -7200
# Node ID 0c1061ea755919e61c13f249156349a64e6c69d9
# Parent  60821dbc9f1827eb58e52f71b63a475647849663
a more modern proof

diff -r 60821dbc9f18 -r 0c1061ea7559 src/HOL/Lex/RegSet_of_nat_DA.ML
--- 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
diff -r 60821dbc9f18 -r 0c1061ea7559 src/HOL/UNITY/Lift.ML
--- 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";