src/Tools/isac/Knowledge/Test.thy
changeset 59360 729c3ca4e5fc
parent 59352 172b53399454
child 59367 fb6f5ef2c647
     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_")),