src/HOL/Fun.thy
changeset 10826 f3b7201dda27
parent 10212 33fe2d701ddd
child 11123 15ffc08f905e
     1.1 --- a/src/HOL/Fun.thy	Mon Jan 08 11:06:24 2001 +0100
     1.2 +++ b/src/HOL/Fun.thy	Mon Jan 08 12:27:36 2001 +0100
     1.3 @@ -88,9 +88,6 @@
     1.4    "lam x:A. f"  == "restrict (%x. f) A"
     1.5  
     1.6  constdefs
     1.7 -  Applyall :: "[('a => 'b) set, 'a]=> 'b set"
     1.8 -    "Applyall F a == (%f. f a) `` F"
     1.9 -
    1.10    compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
    1.11      "compose A g f == lam x : A. g(f x)"
    1.12