src/ZF/UNITY/FP.ML

--- a/src/ZF/UNITY/FP.ML	Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/FP.ML	Tue May 27 11:39:03 2003 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/FP.ML
+(*  Title:      ZF/UNITY/FP.ML
     ID:         $Id$
     Author:     Sidi O Ehmety, Computer Laboratory
     Copyright   2001  University of Cambridge
@@ -28,10 +28,6 @@
 qed "st_set_FP";
 AddIffs [st_set_FP];
 
-Goal "Union(B) Int A = (UN C:B. C Int A)"; 
-by (Blast_tac 1);
-qed "Int_Union2";
-
 Goalw [FP_Orig_def, stable_def] "F:program ==> F:stable(FP_Orig(F) Int B)";
 by (stac Int_Union2 1);
 by (blast_tac (claset() addIs [constrains_UN]) 1);
@@ -44,11 +40,6 @@
 
 bind_thm("FP_Orig_weakest",  allI RS FP_Orig_weakest2);
 
-Goal "A Int cons(a, B) = \
-   \ (if a : A then cons(a, cons(a, (A Int B))) else A Int B)";
-by Auto_tac;
-qed "Int_cons_right";
-
 Goal "F:program ==> F : stable (FP(F) Int B)";
 by (subgoal_tac "FP(F) Int B = (UN x:B. FP(F) Int {x})" 1);
 by (Blast_tac 2);