Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
unused lemma
authornipkow
Tue, 19 Dec 2023 17:30:50 +0100
changeset 79296 f758b4e9d643
parent 79286 366a5ad2f2b3
child 79297 963570d120b2
unused lemma
src/HOL/Int.thy file | annotate | diff | comparison | revisions 
--- 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>
isabelle