proper use of function_package ML files;
authorwenzelm
Tue, 03 Jul 2007 22:27:08 +0200
changeset 23554 151d60fbfffe
parent 23553 af8ae54238f5
child 23555 16e5fd18905c
proper use of function_package ML files;
src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jul 03 22:27:05 2007 +0200
+++ b/src/HOL/List.thy	Tue Jul 03 22:27:08 2007 +0200
@@ -8,6 +8,8 @@
 theory List
 imports PreList
 uses "Tools/string_syntax.ML"
+  ("Tools/function_package/lexicographic_order.ML")
+  ("Tools/function_package/fundef_datatype.ML")
 begin
 
 datatype 'a list =