Removed Applyall
authornipkow
Mon Jan 08 12:27:36 2001 +0100 (2001-01-08)
changeset 10826f3b7201dda27
parent 10825 47c4a76b0c7a
child 10827 a7ac8e1e024b
Removed Applyall
src/HOL/Fun.ML
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.ML	Mon Jan 08 11:06:24 2001 +0100
     1.2 +++ b/src/HOL/Fun.ML	Mon Jan 08 12:27:36 2001 +0100
     1.3 @@ -637,7 +637,7 @@
     1.4  qed "compose_Inv_id";
     1.5  
     1.6  
     1.7 -(*** Pi and Applyall ***)
     1.8 +(*** Pi ***)
     1.9  
    1.10  Goalw [Pi_def] "[| B(x) = {};  x: A |] ==> (PI x: A. B x) = {}";
    1.11  by Auto_tac;
    1.12 @@ -647,14 +647,7 @@
    1.13  by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
    1.14  qed "Pi_total1";
    1.15  
    1.16 -Goal "[| a : A; Pi A B ~= {} |] ==> Applyall (Pi A B) a = B a";
    1.17 -by (auto_tac (claset(), simpset() addsimps [Applyall_def, Pi_def]));
    1.18 -by (rename_tac "g z" 1);
    1.19 -by (res_inst_tac [("x","%y. if  (y = a) then z else g y")] exI 1);
    1.20 -by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1]));
    1.21 -qed "Applyall_beta";
    1.22 -
    1.23 -Goal "Pi {} B = { (%x. @ y. True) }";
    1.24 +Goal "Pi {} B = { %x. @y. True }";
    1.25  by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def]));
    1.26  qed "Pi_empty";
    1.27  
     2.1 --- a/src/HOL/Fun.thy	Mon Jan 08 11:06:24 2001 +0100
     2.2 +++ b/src/HOL/Fun.thy	Mon Jan 08 12:27:36 2001 +0100
     2.3 @@ -88,9 +88,6 @@
     2.4    "lam x:A. f"  == "restrict (%x. f) A"
     2.5  
     2.6  constdefs
     2.7 -  Applyall :: "[('a => 'b) set, 'a]=> 'b set"
     2.8 -    "Applyall F a == (%f. f a) `` F"
     2.9 -
    2.10    compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
    2.11      "compose A g f == lam x : A. g(f x)"
    2.12