# HG changeset patch
# User nipkow
# Date 860675161 -7200
# Node ID 9c4d5fd41c9b234abaebe30c11cfe1deabe04225
# Parent  8658bf6c1a5b9eea6b601109a1c831977b9be128
Deleted stupid proof at the end not needed anywhere.

diff -r 8658bf6c1a5b -r 9c4d5fd41c9b src/HOLCF/ex/Witness.ML
--- a/src/HOLCF/ex/Witness.ML	Thu Apr 10 12:21:21 1997 +0200
+++ b/src/HOLCF/ex/Witness.ML	Thu Apr 10 14:26:01 1997 +0200
@@ -111,19 +111,3 @@
 by (lift.induct_tac "x" 1);
 auto();
 qed "refl_per_one";
-
-(* weq *)
-val prems = goal thy 
-	"[|x~=UU; y~=UU|]==>(x=y-->(x bullet y)=TT)&(x~=y-->(x bullet y)=FF)";
-by(subgoal_tac"x~=UU&y~=UU-->(x=y-->(x bullet y)=TT)&(x~=y-->(x bullet y)=FF)"1);
-by (cut_facts_tac prems 1);
-by (fast_tac HOL_cs 1);
-by (lift.induct_tac "x" 1);
-by (lift.induct_tac "y" 2);
-by (lift.induct_tac "y" 1);
-auto();
-br refl_per_one 1;
-auto();
-by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1);
-result();
-