# HG changeset patch
# User haftmann
# Date 1334515867 -7200
# Node ID be6dd389639df181502747c52ce8239892e7ce00
# Parent  54a2f155621b469313429bc35f2354f624e21787
centralized enriched_type declaration, thanks to in-situ available Isar commands

diff -r 54a2f155621b -r be6dd389639d src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Sun Apr 15 20:41:46 2012 +0200
+++ b/src/HOL/Datatype.thy	Sun Apr 15 20:51:07 2012 +0200
@@ -14,12 +14,6 @@
   ("Tools/Datatype/datatype_realizer.ML")
 begin
 
-subsection {* Prelude: lifting over function space *}
-
-enriched_type map_fun: map_fun
-  by (simp_all add: fun_eq_iff)
-
-
 subsection {* The datatype universe *}
 
 definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}"
@@ -532,3 +526,4 @@
 setup Datatype_Realizer.setup
 
 end
+
diff -r 54a2f155621b -r be6dd389639d src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sun Apr 15 20:41:46 2012 +0200
+++ b/src/HOL/Fun.thy	Sun Apr 15 20:51:07 2012 +0200
@@ -803,4 +803,11 @@
 
 use "Tools/enriched_type.ML"
 
+enriched_type map_fun: map_fun
+  by (simp_all add: fun_eq_iff)
+
+enriched_type vimage
+  by (simp_all add: fun_eq_iff vimage_compose)
+
 end
+
diff -r 54a2f155621b -r be6dd389639d src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Sun Apr 15 20:41:46 2012 +0200
+++ b/src/HOL/Quotient.thy	Sun Apr 15 20:51:07 2012 +0200
@@ -19,13 +19,6 @@
 begin
 
 text {*
-  An aside: contravariant functorial structure of sets.
-*}
-
-enriched_type vimage
-  by (simp_all add: fun_eq_iff vimage_compose)
-
-text {*
   Basic definition for equivalence relations
   that are represented by predicates.
 *}
@@ -911,3 +904,4 @@
   fun_rel (infixr "===>" 55)
 
 end
+