src/HOL/Decision_Procs/mir_tac.ML
changeset 35050 9f841f20dca6
parent 33004 715566791eb0
child 35625 9c818cab0dd0
     1.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Mon Feb 08 17:12:32 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Mon Feb 08 17:12:38 2010 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4               @{thm "real_of_nat_number_of"},
     1.5               @{thm "real_of_nat_Suc"}, @{thm "real_of_nat_one"}, @{thm "real_of_one"},
     1.6               @{thm "real_of_int_zero"}, @{thm "real_of_nat_zero"},
     1.7 -             @{thm "Ring_and_Field.divide_zero"}, 
     1.8 +             @{thm "Fields.divide_zero"}, 
     1.9               @{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"}, 
    1.10               @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
    1.11               @{thm "diff_def"}, @{thm "minus_divide_left"}]