# HG changeset patch
# User haftmann
# Date 1240918488 -7200
# Node ID 506e57123cd18f3d553f5dbe307f86544d91556f
# Parent  aabad7789183edf88750f93fe456aaea21d13fc1
ephermal enforcement of import order to circumvent current problem in merging interpretation morphisms

diff -r aabad7789183 -r 506e57123cd1 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Apr 28 13:34:46 2009 +0200
+++ b/src/HOL/Relation.thy	Tue Apr 28 13:34:48 2009 +0200
@@ -6,7 +6,8 @@
 header {* Relations *}
 
 theory Relation
-imports Datatype Finite_Set
+imports Finite_Set Datatype
+  (*FIXME order is important, otherwise merge problem for canonical interpretation of class monoid_mult wrt. power!*)
 begin
 
 subsection {* Definitions *}