dequalified fact name
authorhaftmann
Fri Apr 23 15:17:59 2010 +0200 (2010-04-23)
changeset 36305dbe99291eb3c
parent 36304 6984744e6b34
child 36306 18c088e1c4ef
dequalified fact name
src/HOL/Groebner_Basis.thy
     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"},