# HG changeset patch
# User paulson
# Date 846859616 -3600
# Node ID 545ac77dab29cc9cb45137811be03cff7ced159a
# Parent  76d5ed939545dfad2d90ac73603eaf99649a1148
Proof of antisym_less_lift now simpler and more robust

diff -r 76d5ed939545 -r 545ac77dab29 src/HOLCF/Lift1.ML
--- a/src/HOLCF/Lift1.ML	Fri Nov 01 15:45:50 1996 +0100
+++ b/src/HOLCF/Lift1.ML	Fri Nov 01 15:46:56 1996 +0100
@@ -133,15 +133,13 @@
         ]);
 
 qed_goal "antisym_less_lift"  Lift1.thy 
-        "[|less_lift p1 p2;less_lift p2 p1|] ==> p1=p2"
- (fn prems =>
+        "!!p1. [|less_lift p1 p2;less_lift p2 p1|] ==> p1=p2"
+ (fn _ =>
         [
-        (cut_facts_tac prems 1),
         (res_inst_tac [("p","p1")] liftE 1),
         (hyp_subst_tac 1),
         (res_inst_tac [("p","p2")] liftE 1),
-        (hyp_subst_tac 1),
-        (rtac refl 1),
+        (etac sym 1),
         (hyp_subst_tac 1),
         (res_inst_tac [("P","less_lift (Iup x) UU_lift")] notE 1),
         (rtac less_lift1b 1),