--- 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
+
--- 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
+
--- 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
+