src/HOL/Groebner_Basis.thy
changeset 35050 9f841f20dca6
parent 34974 18b41bba42b5
child 35084 e25eedfc15ce
     1.1 --- a/src/HOL/Groebner_Basis.thy	Mon Feb 08 17:12:32 2010 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Feb 08 17:12:38 2010 +0100
     1.3 @@ -621,7 +621,7 @@
     1.4  
     1.5  val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
     1.6             @{thm "divide_Numeral1"},
     1.7 -           @{thm "Ring_and_Field.divide_zero"}, @{thm "divide_Numeral0"},
     1.8 +           @{thm "Fields.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"},