[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:

lemma arith_example:
  "[|(i::int) < (nb - 1) mod 256;
    0 <= nb;
    nb < 256;
    0 <= i;
    i < 256|]
   ==> i < (i + 1) mod 256"
apply arith

I'm running the Isabelle_08-Feb-2006 snapshot.

Thanks,
-john





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.