--- a/src/HOL/List.thy Fri Feb 20 17:57:16 1998 +0100
+++ b/src/HOL/List.thy Sun Feb 22 14:12:23 1998 +0100
@@ -6,7 +6,7 @@
The datatype of finite lists.
*)
-List = Divides +
+List = WF_Rel +
datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)