# HG changeset patch
# User lcp
# Date 783614754 -3600
# Node ID 2342e70a97d4c544ca370bce67c16cdb64a689a1
# Parent  370653a155355f18fee3957e9c678969fd8dc2ff
ZF/OrderArith/thin: deleted as obsolete
ZF/OrderArith/wf_on_radd: now uses thin_rl

diff -r 370653a15535 -r 2342e70a97d4 src/ZF/OrderArith.ML
--- a/src/ZF/OrderArith.ML	Mon Oct 31 15:41:20 1994 +0100
+++ b/src/ZF/OrderArith.ML	Mon Oct 31 15:45:54 1994 +0100
@@ -6,10 +6,6 @@
 Towards ordinal arithmetic 
 *)
 
-(*for deleting an unwanted assumption*)
-val thin = prove_goal pure_thy "[| PROP P; PROP Q |] ==> PROP Q"
-     (fn prems => [resolve_tac prems 1]);
-
 open OrderArith;
 
 
@@ -86,7 +82,7 @@
 by (rtac wf_onI2 1);
 by (subgoal_tac "ALL x:A. Inl(x): Ba" 1);
 (*Proving the lemma, which is needed twice!*)
-by (eres_inst_tac [("P", "y : A + B")] thin 2);
+by (eres_inst_tac [("V", "y : A + B")] thin_rl 2);
 by (rtac ballI 2);
 by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2);
 by (etac (bspec RS mp) 2);