# HG changeset patch
# User paulson
# Date 864998204 -7200
# Node ID 832c245d967c066f32f755a902b4357052260ea9
# Parent  2402c6ab1561f0bfda901c17da02c4447eadd5a6
Now Divides must be the parent

diff -r 2402c6ab1561 -r 832c245d967c src/HOL/Finite.thy
--- a/src/HOL/Finite.thy	Fri May 30 15:15:57 1997 +0200
+++ b/src/HOL/Finite.thy	Fri May 30 15:16:44 1997 +0200
@@ -6,7 +6,7 @@
 Finite sets and their cardinality
 *)
 
-Finite = Arith +
+Finite = Divides +
 
 consts Fin :: 'a set => 'a set set
 
diff -r 2402c6ab1561 -r 832c245d967c src/HOL/List.thy
--- a/src/HOL/List.thy	Fri May 30 15:15:57 1997 +0200
+++ b/src/HOL/List.thy	Fri May 30 15:16:44 1997 +0200
@@ -6,7 +6,7 @@
 The datatype of finite lists.
 *)
 
-List = Arith +
+List = Divides +
 
 datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)