fixed compose decl;
authorwenzelm
Thu Jul 13 23:08:42 2000 +0200 (2000-07-13)
changeset 93094078d5e8b293
parent 9308 4adf25becaa4
child 9310 ab706fdb0842
fixed compose decl;
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.thy	Thu Jul 13 23:08:20 2000 +0200
     1.2 +++ b/src/HOL/Fun.thy	Thu Jul 13 23:08:42 2000 +0200
     1.3 @@ -81,7 +81,7 @@
     1.4    Applyall :: "[('a => 'b) set, 'a]=> 'b set"
     1.5      "Applyall F a == (%f. f a) `` F"
     1.6  
     1.7 -  compose :: "['a set, 'a => 'b, 'b => 'c] => ('a => 'c)"
     1.8 +  compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
     1.9      "compose A g f == lam x : A. g(f x)"
    1.10  
    1.11    Inv    :: "['a set, 'a => 'b] => ('b => 'a)"