summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Algebra/IntRing.thy

changeset 29242 | e190bc2a5399 |

parent 29237 | e90d9d51106b |

child 29424 | 948d616959e4 |

1.1 --- a/src/HOL/Algebra/IntRing.thy Thu Dec 18 20:19:49 2008 +0100 1.2 +++ b/src/HOL/Algebra/IntRing.thy Fri Dec 19 11:09:09 2008 +0100 1.3 @@ -328,7 +328,7 @@ 1.4 next 1.5 assume "UNIV = {uu. EX x. uu = x * p}" 1.6 from this obtain x 1.7 - where "1 = x * p" by fast 1.8 + where "1 = x * p" by best 1.9 from this [symmetric] 1.10 have "p * x = 1" by (subst zmult_commute) 1.11 hence "\<bar>p * x\<bar> = 1" by simp