# HG changeset patch
# User obua
# Date 1127573021 -7200
# Node ID f4e2587bc7a5a702f278dea8f4c5d69ba2843936
# Parent  ff1923b1978b4800ae35832e8adeaff751f7747b
HOL4-Import: map ONTO to Fun.surj

diff -r ff1923b1978b -r f4e2587bc7a5 src/HOL/Import/Generate-HOL/GenHOL4Base.thy
--- 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;