1.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Feb 08 13:20:40 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Test.thy Fri Feb 09 11:16:05 2018 +0100
1.3 @@ -403,7 +403,7 @@
1.4 thus they MUST be done IMMEDIATELY before calc *)
1.5 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.6 Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.7 - Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
1.8 + Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
1.9 Calc ("Atools.pow", eval_binop "#power_"),
1.10
1.11 Thm ("rcollect_right",num_str @{thm rcollect_right}),
1.12 @@ -481,7 +481,7 @@
1.13 (*aus Atools.ML*)
1.14 ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
1.15 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
1.16 - ("DIVIDE" ,("Fields.inverse_class.divide" ,eval_cancel "#divide_e")),
1.17 + ("DIVIDE" ,("Rings.divide_class.divide" ,eval_cancel "#divide_e")),
1.18 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
1.19 ("is_const",("Atools.is'_const",eval_const "#is_const_")),
1.20 ("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),