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.
Theorem "(x::int) dvd 1 = ( ¦x¦ = 1)" added to default simpset.
authorchaieb
Fri, 19 Jan 2007 15:13:47 +0100
changeset 22091 d13ad9a479f9
parent 22090 bc8aee017f8a
child 22092 ab3dfcef6489
Theorem "(x::int) dvd 1 = ( ¦x¦ = 1)" added to default simpset. This solves the goals like "~ 4 dvd 1". This used to fail before.
src/HOL/Integ/IntDiv.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Integ/IntDiv.thy	Fri Jan 19 13:16:37 2007 +0100
+++ b/src/HOL/Integ/IntDiv.thy	Fri Jan 19 15:13:47 2007 +0100
@@ -1243,7 +1243,7 @@
   apply (simp add: mult_ac)
   done
 
-lemma zdvd1_eq: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
+lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
 proof
   assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)
   hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
isabelle