# HG changeset patch # User chaieb # Date 1169216027 -3600 # Node ID d13ad9a479f9ae32589ab2783479fa7b39ebc537 # Parent bc8aee017f8a7fea1b5ee7224284dce59998589d Theorem "(x::int) dvd 1 = ( ¦x¦ = 1)" added to default simpset. This solves the goals like "~ 4 dvd 1". This used to fail before. diff -r bc8aee017f8a -r d13ad9a479f9 src/HOL/Integ/IntDiv.thy --- 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 = ( \x\ = 1)" +lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \x\ = 1)" proof assume d: "x dvd 1" hence "int (nat \x\) dvd int (nat 1)" by (simp add: zdvd_abs1) hence "nat \x\ dvd 1" by (simp add: zdvd_int)