Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed compose decl;
authorwenzelm
Thu, 13 Jul 2000 23:08:42 +0200
changeset 9309 4078d5e8b293
parent 9308 4adf25becaa4
child 9310 ab706fdb0842
fixed compose decl;
src/HOL/Fun.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Fun.thy	Thu Jul 13 23:08:20 2000 +0200
+++ b/src/HOL/Fun.thy	Thu Jul 13 23:08:42 2000 +0200
@@ -81,7 +81,7 @@
   Applyall :: "[('a => 'b) set, 'a]=> 'b set"
     "Applyall F a == (%f. f a) `` F"
 
-  compose :: "['a set, 'a => 'b, 'b => 'c] => ('a => 'c)"
+  compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
     "compose A g f == lam x : A. g(f x)"
 
   Inv    :: "['a set, 'a => 'b] => ('b => 'a)"
isabelle