1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Wed Dec 05 10:21:35 2012 +0100
1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Wed Dec 05 15:29:36 2012 +0100
1.3 @@ -55,7 +55,7 @@
1.4 [Thm ("real_assoc_1",num_str @{thm real_assoc_1})
1.5 (*
1.6 Don't use
1.7 - Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
1.8 + Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
1.9 Calc ("Atools.pow" ,eval_binop "#power_"),
1.10 *)
1.11 ];
1.12 @@ -66,7 +66,7 @@
1.13 [Thm ("real_assoc_1",num_str @{thm real_assoc_1})
1.14 (*
1.15 Don't use
1.16 - Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
1.17 + Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
1.18 Calc ("Atools.pow" ,eval_binop "#power_"),
1.19 *)
1.20 ];
1.21 @@ -87,7 +87,7 @@
1.22 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
1.23 Calc ("Groups.times_class.times",eval_binop "#mult_"),
1.24 (* Dont use
1.25 - Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
1.26 + Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
1.27 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
1.28 *)
1.29 Calc ("Atools.pow" ,eval_binop "#power_")