made List.thy a join point in the theory graph
authorhaftmann
Fri, 18 Jun 2010 09:21:41 +0200
changeset 37457 7201c7e0db87
parent 37453 44a307746163
child 37458 4a76497f2eaa
made List.thy a join point in the theory graph
src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jun 18 09:04:00 2010 +0200
+++ b/src/HOL/List.thy	Fri Jun 18 09:21:41 2010 +0200
@@ -5,7 +5,7 @@
 header {* The datatype of finite lists *}
 
 theory List
-imports Plain Presburger Sledgehammer Recdef
+imports Plain Quotient Presburger Code_Numeral Sledgehammer Recdef
 uses ("Tools/list_code.ML")
 begin