# HG changeset patch
# User nipkow
# Date 1703003450 -3600
# Node ID f758b4e9d64320d0bdab09395fee15f52893e0dc
# Parent  366a5ad2f2b337e8dfa8f5668c092583931bc134
unused lemma

diff -r 366a5ad2f2b3 -r f758b4e9d643 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Dec 18 22:49:33 2023 +0100
+++ b/src/HOL/Int.thy	Tue Dec 19 17:30:50 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>