# HG changeset patch
# User nipkow
# Date 1703023257 -3600
# Node ID 963570d120b22a2d8a5a3b04b5a81036d6767a5e
# Parent  123651f3ec5d9ea0d8d72c769679d5f3f89572cb# Parent  f758b4e9d64320d0bdab09395fee15f52893e0dc
merged

diff -r 123651f3ec5d -r 963570d120b2 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Dec 19 18:51:32 2023 +0100
+++ b/src/HOL/Int.thy	Tue Dec 19 23:00:57 2023 +0100
@@ -25,10 +25,6 @@
   show "transp intrel" by (auto simp: transp_def)
 qed
 
-lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
-  "(\<And>x y. z = Abs_Integ (x, y) \<Longrightarrow> P) \<Longrightarrow> P"
-  by (induct z) auto
-
 
 subsection \<open>Integers form a commutative ring\<close>