diff -r 0a2f744e008a -r 858ab9a9b047 src/ZF/arith.thy --- a/src/ZF/arith.thy Tue Nov 16 14:23:19 1993 +0100 +++ b/src/ZF/arith.thy Tue Nov 16 14:24:21 1993 +0100 @@ -6,7 +6,7 @@ Arithmetic operators and their definitions *) -Arith = Epsilon + +Arith = Epsilon + "simpdata" + consts rec :: "[i, i, [i,i]=>i]=>i" "#*" :: "[i,i]=>i" (infixl 70)