src/HOL/Rings.thy
changeset 63040 eb4ddd18d635
parent 62626 de25474ce728
child 63325 1086d56cde86
     1.1 --- a/src/HOL/Rings.thy	Sun Apr 24 21:31:14 2016 +0200
     1.2 +++ b/src/HOL/Rings.thy	Mon Apr 25 16:09:26 2016 +0200
     1.3 @@ -847,7 +847,7 @@
     1.4      and "is_unit b" and "1 div a = b" and "1 div b = a"
     1.5      and "a * b = 1" and "c div a = c * b"
     1.6  proof (rule that)
     1.7 -  def b \<equiv> "1 div a"
     1.8 +  define b where "b = 1 div a"
     1.9    then show "1 div a = b" by simp
    1.10    from b_def \<open>is_unit a\<close> show "is_unit b" by simp
    1.11    from \<open>is_unit a\<close> and \<open>is_unit b\<close> show "a \<noteq> 0" and "b \<noteq> 0" by auto