src/ZF/func.ML

--- a/src/ZF/func.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/func.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -53,11 +53,11 @@
 
 (*Empty function spaces*)
 goalw thy [Pi_def, function_def] "Pi(0,A) = {0}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Pi_empty1";
 
 goalw thy [Pi_def] "!!A a. a:A ==> A->0 = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Pi_empty2";
 
 (*The empty function*)
@@ -67,7 +67,7 @@
 
 (*The singleton function*)
 goalw thy [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "singleton_fun";
 
 Addsimps [empty_fun, singleton_fun];
@@ -245,7 +245,7 @@
 (** Images of functions **)
 
 goalw thy [lam_def] "!!C A. C <= A ==> (lam x:A.b(x)) `` C = {b(x). x:C}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "image_lam";
 
 goal thy "!!C A. [| f : Pi(A,B);  C <= A |] ==> f``C = {f`x. x:C}";
@@ -291,7 +291,7 @@
 qed "restrict_eqI";
 
 goalw thy [restrict_def, lam_def] "domain(restrict(f,C)) = C";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "domain_restrict";
 
 val [prem] = goalw thy [restrict_def]
@@ -360,7 +360,7 @@
 (** Domain and range of a function/relation **)
 
 goalw thy [Pi_def] "!!f. f : Pi(A,B) ==> domain(f)=A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "domain_of_fun";
 
 goal thy "!!f. [| f : Pi(A,B);  a: A |] ==> f`a : range(f)";
@@ -379,7 +379,7 @@
     "!!f A B. [| 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 (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "fun_extend";
 
 goal thy
@@ -417,6 +417,6 @@
 by (etac consE 1);
 by (ALLGOALS 
     (asm_simp_tac (!simpset addsimps [restrict, fun_extend_apply1, 
-				      fun_extend_apply2])));
+                                      fun_extend_apply2])));
 qed "cons_fun_eq";