1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Dec 05 10:21:35 2012 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Dec 05 15:29:36 2012 +0100
1.3 @@ -200,7 +200,7 @@
1.4 Thm ("divide_divide_eq_left",
1.5 num_str @{thm divide_divide_eq_left}),
1.6 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.7 - Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"),
1.8 + Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e"),
1.9
1.10 Thm ("rat_power", num_str @{thm rat_power})
1.11 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
1.12 @@ -264,7 +264,7 @@
1.13 Rls_ discard_parentheses,
1.14 (*Rls_ collect_bdv, from make_polynomial_in*)
1.15 Rls_ separate_bdv2,
1.16 - Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e")
1.17 + Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e")
1.18 ],
1.19 scr = EmptyScr}:rls;
1.20
1.21 @@ -302,7 +302,7 @@
1.22 * num_str @{thm add_divide_distrib})
1.23 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
1.24 * ]),
1.25 -* Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e")
1.26 +* Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e")
1.27 * ],
1.28 * scr = EmptyScr
1.29 * }:rls);