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.
All datatypes now require Arith.
authornipkow
Fri, 23 May 1997 09:18:06 +0200
changeset 3309 992a25b24d0d
parent 3308 da002cef7090
child 3310 0ceaad3c3f52
All datatypes now require Arith.
src/HOL/Induct/Comb.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Induct/Comb.thy	Fri May 23 09:17:26 1997 +0200
+++ b/src/HOL/Induct/Comb.thy	Fri May 23 09:18:06 1997 +0200
@@ -13,7 +13,7 @@
 *)
 
 
-Comb = Trancl +
+Comb = Arith +
 
 (** Datatype definition of combinators S and K, with infixed application **)
 datatype comb = K
isabelle