author | wenzelm |
Tue, 03 Jul 2007 22:27:08 +0200 | |
changeset 23554 | 151d60fbfffe |
parent 23553 | af8ae54238f5 |
child 23555 | 16e5fd18905c |
src/HOL/List.thy | file | annotate | diff | comparison | revisions |
--- 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 =