Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Now Divides must be the parent
authorpaulson
Fri, 30 May 1997 15:16:44 +0200
changeset 3367 832c245d967c
parent 3366 2402c6ab1561
child 3368 be517d000c02
Now Divides must be the parent
src/HOL/Finite.thy file | annotate | diff | comparison | revisions
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- 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
 
--- 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)
isabelle