# HG changeset patch
# User huffman
# Date 1158422654 -7200
# Node ID 7ced6152e52c81664c9712ce5b17ecc56771fdce
# Parent  2c31dd358c2109d6c62f5cd1c28adaca949c7eca
int_diff_cases moved to Integ/IntDef.thy

diff -r 2c31dd358c21 -r 7ced6152e52c src/HOL/Hyperreal/StarClasses.thy
--- a/src/HOL/Hyperreal/StarClasses.thy	Sat Sep 16 02:40:00 2006 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy	Sat Sep 16 18:04:14 2006 +0200
@@ -380,13 +380,6 @@
 lemma star_of_of_nat [simp]: "star_of (of_nat n) = of_nat n"
 by transfer (rule refl)
 
-lemma int_diff_cases:
-assumes prem: "\<And>m n. z = int m - int n \<Longrightarrow> 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 -- "Belongs in Integ/IntDef.thy"
-
 lemma star_of_int_def [transfer_unfold]: "of_int z \<equiv> star_of (of_int z)"
 by (rule eq_reflection, rule_tac z=z in int_diff_cases, simp)