src/HOL/NSA/StarDef.thy
changeset 60429 d3d1e185cd63
parent 60353 838025c6e278
child 60516 0826b7025d07
     1.1 --- a/src/HOL/NSA/StarDef.thy	Thu Jun 11 21:41:55 2015 +0100
     1.2 +++ b/src/HOL/NSA/StarDef.thy	Fri Jun 12 08:53:23 2015 +0200
     1.3 @@ -577,7 +577,7 @@
     1.4  lemma Standard_mult: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x * y \<in> Standard"
     1.5  by (simp add: star_mult_def)
     1.6  
     1.7 -lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> divide x y \<in> Standard"
     1.8 +lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x / y \<in> Standard"
     1.9  by (simp add: star_divide_def)
    1.10  
    1.11  lemma Standard_inverse: "x \<in> Standard \<Longrightarrow> inverse x \<in> Standard"
    1.12 @@ -855,9 +855,9 @@
    1.13  instance star :: (semidom) semidom ..
    1.14  instance star :: (semidom_divide) semidom_divide
    1.15  proof
    1.16 -  show "\<And>b a :: 'a star. b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
    1.17 +  show "\<And>b a :: 'a star. b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
    1.18      by transfer simp
    1.19 -  show "\<And>a :: 'a star. divide a 0 = 0"
    1.20 +  show "\<And>a :: 'a star. a div 0 = 0"
    1.21      by transfer simp
    1.22  qed
    1.23  instance star :: (semiring_div) semiring_div