ephermal enforcement of import order to circumvent current problem in merging interpretation morphisms
authorhaftmann
Tue Apr 28 13:34:48 2009 +0200 (2009-04-28)
changeset 31011506e57123cd1
parent 31010 aabad7789183
child 31012 751f5aa3e315
ephermal enforcement of import order to circumvent current problem in merging interpretation morphisms
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Tue Apr 28 13:34:46 2009 +0200
     1.2 +++ b/src/HOL/Relation.thy	Tue Apr 28 13:34:48 2009 +0200
     1.3 @@ -6,7 +6,8 @@
     1.4  header {* Relations *}
     1.5  
     1.6  theory Relation
     1.7 -imports Datatype Finite_Set
     1.8 +imports Finite_Set Datatype
     1.9 +  (*FIXME order is important, otherwise merge problem for canonical interpretation of class monoid_mult wrt. power!*)
    1.10  begin
    1.11  
    1.12  subsection {* Definitions *}