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; 