# 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 *}