--- a/NEWS Tue Oct 26 16:56:54 2010 +0200
+++ b/NEWS Tue Oct 26 16:59:19 2010 +0200
@@ -77,7 +77,7 @@
*** HOL ***
* New command 'partial_function' provides basic support for recursive
-function definitons over complete partial orders. Concrete instances
+function definitions over complete partial orders. Concrete instances
are provided for i) the option type, ii) tail recursion on arbitrary
types, and iii) the heap monad of Imperative_HOL. See
HOL/ex/Fundefs.thy and HOL/Imperative_HOL/ex/Linked_Lists.thy for
--- a/src/HOL/List.thy Tue Oct 26 16:56:54 2010 +0200
+++ b/src/HOL/List.thy Tue Oct 26 16:59:19 2010 +0200
@@ -5,7 +5,7 @@
header {* The datatype of finite lists *}
theory List
-imports Plain Presburger Recdef Code_Numeral Quotient
+imports Plain Presburger Recdef Code_Numeral Quotient ATP
uses ("Tools/list_code.ML")
begin