# HG changeset patch
# User nipkow
# Date 864371886 -7200
# Node ID 992a25b24d0d20909e5dd10a0501f89a28f863f8
# Parent  da002cef70901c5cd513fa351207812e992c7585
All datatypes now require Arith.

diff -r da002cef7090 -r 992a25b24d0d src/HOL/Induct/Comb.thy
--- 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