# HG changeset patch
# User nipkow
# Date 978953256 -3600
# Node ID f3b7201dda27f559650011be2ecd1f8abd43f26e
# Parent  47c4a76b0c7aa771cf97a67bd7cad3c206eff3b0
Removed Applyall

diff -r 47c4a76b0c7a -r f3b7201dda27 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Mon Jan 08 11:06:24 2001 +0100
+++ b/src/HOL/Fun.ML	Mon Jan 08 12:27:36 2001 +0100
@@ -637,7 +637,7 @@
 qed "compose_Inv_id";
 
 
-(*** Pi and Applyall ***)
+(*** Pi ***)
 
 Goalw [Pi_def] "[| B(x) = {};  x: A |] ==> (PI x: A. B x) = {}";
 by Auto_tac;
@@ -647,14 +647,7 @@
 by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
 qed "Pi_total1";
 
-Goal "[| a : A; Pi A B ~= {} |] ==> Applyall (Pi A B) a = B a";
-by (auto_tac (claset(), simpset() addsimps [Applyall_def, Pi_def]));
-by (rename_tac "g z" 1);
-by (res_inst_tac [("x","%y. if  (y = a) then z else g y")] exI 1);
-by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1]));
-qed "Applyall_beta";
-
-Goal "Pi {} B = { (%x. @ y. True) }";
+Goal "Pi {} B = { %x. @y. True }";
 by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def]));
 qed "Pi_empty";
 
diff -r 47c4a76b0c7a -r f3b7201dda27 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Jan 08 11:06:24 2001 +0100
+++ b/src/HOL/Fun.thy	Mon Jan 08 12:27:36 2001 +0100
@@ -88,9 +88,6 @@
   "lam x:A. f"  == "restrict (%x. f) A"
 
 constdefs
-  Applyall :: "[('a => 'b) set, 'a]=> 'b set"
-    "Applyall F a == (%f. f a) `` F"
-
   compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
     "compose A g f == lam x : A. g(f x)"