summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Rings.thy

changeset 63040 | eb4ddd18d635 |

parent 62626 | de25474ce728 |

child 63325 | 1086d56cde86 |

--- a/src/HOL/Rings.thy Sun Apr 24 21:31:14 2016 +0200 +++ b/src/HOL/Rings.thy Mon Apr 25 16:09:26 2016 +0200 @@ -847,7 +847,7 @@ and "is_unit b" and "1 div a = b" and "1 div b = a" and "a * b = 1" and "c div a = c * b" proof (rule that) - def b \<equiv> "1 div a" + define b where "b = 1 div a" then show "1 div a = b" by simp from b_def \<open>is_unit a\<close> show "is_unit b" by simp from \<open>is_unit a\<close> and \<open>is_unit b\<close> show "a \<noteq> 0" and "b \<noteq> 0" by auto