# HG changeset patch
# User paulson
# Date 920974141 -3600
# Node ID ca52347e259a4c12566750d3bda8786c5e673821
# Parent  76f3865a2b1d3c674aafe22e3afb8c62ebcddc7f
tidied

diff -r 76f3865a2b1d -r ca52347e259a src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Tue Mar 09 11:01:39 1999 +0100
+++ b/src/HOL/UNITY/Extend.ML	Tue Mar 09 11:09:01 1999 +0100
@@ -8,21 +8,6 @@
   function g (forgotten) maps the extended state to the "extending part"
 *)
 
-    Goal "inj f ==> (f a : f``A) = (a : A)";
-    by (blast_tac (claset() addDs [injD]) 1);
-    qed "inj_image_mem_iff";
-
-
-		Goal "inj f ==> (f``A = f``B) = (A = B)";
-		by (blast_tac (claset() addSEs [equalityE]
-					addDs [injD]) 1);
-		qed "inj_image_eq_iff";
-
-
-val rinst = read_instantiate_sg (sign_of thy);
-
-    (*** General lemmas ***)
-
 Open_locale "Extend";
 
 val slice_def = thm "slice_def";
diff -r 76f3865a2b1d -r ca52347e259a src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Tue Mar 09 11:01:39 1999 +0100
+++ b/src/HOL/UNITY/Union.ML	Tue Mar 09 11:09:01 1999 +0100
@@ -8,14 +8,6 @@
 From Misra's Chapter 5: Asynchronous Compositions of Programs
 *)
 
-
-Goal "k:I ==> (INT i:I. A i) Int A k = (INT i:I. A i)";
-by (Blast_tac 1);
-qed "INT_absorb2";
-
-
-val rinst = read_instantiate_sg (sign_of thy);
-
 Addcongs [UN_cong, INT_cong];