src/HOL/Groebner_Basis.thy
changeset 36305 dbe99291eb3c
parent 35410 1ea89d2a1bd4
child 36349 39be26d1bc28
     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri Apr 23 15:17:59 2010 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Fri Apr 23 15:17:59 2010 +0200
     1.3 @@ -627,7 +627,7 @@
     1.4  
     1.5  val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
     1.6             @{thm "divide_Numeral1"},
     1.7 -           @{thm "Fields.divide_zero"}, @{thm "divide_Numeral0"},
     1.8 +           @{thm "divide_zero"}, @{thm "divide_Numeral0"},
     1.9             @{thm "divide_divide_eq_left"}, @{thm "mult_frac_frac"},
    1.10             @{thm "mult_num_frac"}, @{thm "mult_frac_num"},
    1.11             @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"},