--- a/src/HOL/PreList.thy Tue Sep 18 05:42:46 2007 +0200
+++ b/src/HOL/PreList.thy Tue Sep 18 06:21:40 2007 +0200
@@ -8,6 +8,8 @@
theory PreList
imports Presburger Relation_Power SAT Recdef Extraction Record
+uses "Tools/function_package/lexicographic_order.ML"
+ "Tools/function_package/fundef_datatype.ML"
begin
text {*
@@ -15,5 +17,9 @@
theory ToyList in the documentation.
*}
+(* The lexicographic_order method and the "fun" command *)
+setup LexicographicOrder.setup
+setup FundefDatatype.setup
+
end