--- 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";
--- 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];