src/ZF/func.ML

--- a/src/ZF/func.ML	Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/func.ML	Fri Aug 14 18:37:28 1998 +0200
@@ -389,25 +389,23 @@
 
 (*** Extensions of functions ***)
 
-goal ZF.thy
-    "!!f A B. [| f: A->B;  c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
+Goal "[| f: A->B;  c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
 by (forward_tac [singleton_fun RS fun_disjoint_Un] 1);
 by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2);
 by (Blast_tac 1);
 qed "fun_extend";
 
-goal ZF.thy
-    "!!f A B. [| f: A->B;  c~:A;  b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B";
+Goal "[| f: A->B;  c~:A;  b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B";
 by (blast_tac (claset() addIs [fun_extend RS fun_weaken_type]) 1);
 qed "fun_extend3";
 
-goal ZF.thy "!!f A B. [| f: A->B;  a:A;  c~:A |] ==> cons(<c,b>,f)`a = f`a";
+Goal "[| f: A->B;  a:A;  c~:A |] ==> cons(<c,b>,f)`a = f`a";
 by (rtac (apply_Pair RS consI2 RS apply_equality) 1);
 by (rtac fun_extend 3);
 by (REPEAT (assume_tac 1));
 qed "fun_extend_apply1";
 
-goal ZF.thy "!!f A B. [| f: A->B;  c~:A |] ==> cons(<c,b>,f)`c = b";
+Goal "[| f: A->B;  c~:A |] ==> cons(<c,b>,f)`c = b";
 by (rtac (consI1 RS apply_equality) 1);
 by (rtac fun_extend 1);
 by (REPEAT (assume_tac 1));
@@ -417,8 +415,7 @@
 Addsimps [singleton_apply];
 
 (*For Finite.ML.  Inclusion of right into left is easy*)
-goal ZF.thy
-    "!!c. c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})";
+Goal "c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})";
 by (rtac equalityI 1);
 by (safe_tac (claset() addSEs [fun_extend3]));
 (*Inclusion of left into right*)