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.
HOL4-Import: map ONTO to Fun.surj
authorobua
Sat, 24 Sep 2005 16:43:41 +0200
changeset 17628 f4e2587bc7a5
parent 17627 ff1923b1978b
child 17629 f8ea8068c6d9
HOL4-Import: map ONTO to Fun.surj
src/HOL/Import/Generate-HOL/GenHOL4Base.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sat Sep 24 13:54:35 2005 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sat Sep 24 16:43:41 2005 +0200
@@ -25,7 +25,7 @@
   COND            > HOL.If
   bool_case       > Datatype.bool.bool_case
   ONE_ONE         > HOL4Setup.ONE_ONE
-  ONTO            > HOL4Setup.ONTO
+  ONTO            > Fun.surj
   TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION
   LET             > HOL4Compat.LET;
isabelle