src/HOL/Library/RBT.thy
changeset 30738 0842e906300c
parent 30235 58d147683393
child 32237 cdc76a42fed4
--- a/src/HOL/Library/RBT.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Library/RBT.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      RBT.thy
-    ID:         $Id$
     Author:     Markus Reiter, TU Muenchen
     Author:     Alexander Krauss, TU Muenchen
 *)
@@ -8,7 +7,7 @@
 
 (*<*)
 theory RBT
-imports Plain AssocList
+imports Main AssocList
 begin
 
 datatype color = R | B