[isabelle] arith tactic
Hi, I've run into a problem using the arith tactic. I ran arith for
over 15 minutes on the following subgoal, without success:
"[|(i::int) < (nb - 1) mod 256;
0 <= nb;
nb < 256;
0 <= i;
i < 256|]
==> i < (i + 1) mod 256"
I'm running the Isabelle_08-Feb-2006 snapshot.
This archive was generated by a fusion of
Pipermail (Mailman edition) and