--- a/src/HOL/Integ/IntDef.thy Wed Mar 02 00:56:41 2005 +0100
+++ b/src/HOL/Integ/IntDef.thy Wed Mar 02 10:02:21 2005 +0100
@@ -836,6 +836,13 @@
"[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z"
by (cases z) auto
+text{*Contributed by Brian Huffman*}
+theorem int_diff_cases [case_names diff]:
+assumes prem: "!!m n. z = int m - int n ==> P" shows "P"
+ apply (rule_tac z=z in int_cases)
+ apply (rule_tac m=n and n=0 in prem, simp)
+ apply (rule_tac m=0 and n="Suc n" in prem, simp)
+done
lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
apply (cases z)