equal
deleted
inserted
replaced
52 |
52 |
53 "n div 2 + (n+1) div 2 = (n::nat)" |
53 "n div 2 + (n+1) div 2 = (n::nat)" |
54 |
54 |
55 * simp's arithmetic capabilities have been enhanced a bit: it now |
55 * simp's arithmetic capabilities have been enhanced a bit: it now |
56 takes ~= in premises into account (by performing a case split); |
56 takes ~= in premises into account (by performing a case split); |
|
57 |
|
58 * simp reduces "m*(n div m) + n mod m" to n, even if the two summands are |
|
59 distributed over a sum of terms. |
57 |
60 |
58 |
61 |
59 *** ML *** |
62 *** ML *** |
60 |
63 |
61 * Pure: Tactic.prove provides sane interface for internal proofs; |
64 * Pure: Tactic.prove provides sane interface for internal proofs; |