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