1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Sun Feb 25 16:31:17 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Fri Mar 02 14:19:59 2018 +0100
1.3 @@ -41,17 +41,17 @@
1.4 Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
1.5 Calc ("Atools.occurs'_in",eval_occurs_in ""),
1.6 Calc ("Atools.ident",eval_ident "#ident_"),
1.7 - Thm ("not_true",num_str @{thm not_true}),
1.8 - Thm ("not_false",num_str @{thm not_false}),
1.9 - Thm ("and_true",num_str @{thm and_true}),
1.10 - Thm ("and_false",num_str @{thm and_false}),
1.11 - Thm ("or_true",num_str @{thm or_true}),
1.12 - Thm ("or_false",num_str @{thm or_false})
1.13 + Thm ("not_true",TermC.num_str @{thm not_true}),
1.14 + Thm ("not_false",TermC.num_str @{thm not_false}),
1.15 + Thm ("and_true",TermC.num_str @{thm and_true}),
1.16 + Thm ("and_false",TermC.num_str @{thm and_false}),
1.17 + Thm ("or_true",TermC.num_str @{thm or_true}),
1.18 + Thm ("or_false",TermC.num_str @{thm or_false})
1.19 ];
1.20 (* ----- erls ----- *)
1.21 val LinEq_crls =
1.22 append_rls "LinEq_crls" poly_crls
1.23 - [Thm ("real_assoc_1",num_str @{thm real_assoc_1})
1.24 + [Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1})
1.25 (*
1.26 Don't use
1.27 Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
1.28 @@ -62,7 +62,7 @@
1.29 (* ----- crls ----- *)
1.30 val LinEq_erls =
1.31 append_rls "LinEq_erls" Poly_erls
1.32 - [Thm ("real_assoc_1",num_str @{thm real_assoc_1})
1.33 + [Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1})
1.34 (*
1.35 Don't use
1.36 Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
1.37 @@ -81,7 +81,7 @@
1.38 srls = Erls,
1.39 calc = [], errpatts = [],
1.40 rules = [
1.41 - Thm ("real_assoc_1",num_str @{thm real_assoc_1}),
1.42 + Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}),
1.43 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
1.44 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
1.45 Calc ("Groups.times_class.times",eval_binop "#mult_"),
1.46 @@ -105,11 +105,11 @@
1.47 srls = Erls,
1.48 calc = [], errpatts = [],
1.49 rules = [
1.50 - Thm("lin_isolate_add1",num_str @{thm lin_isolate_add1}),
1.51 + Thm("lin_isolate_add1",TermC.num_str @{thm lin_isolate_add1}),
1.52 (* a+bx=0 -> bx=-a *)
1.53 - Thm("lin_isolate_add2",num_str @{thm lin_isolate_add2}),
1.54 + Thm("lin_isolate_add2",TermC.num_str @{thm lin_isolate_add2}),
1.55 (* a+ x=0 -> x=-a *)
1.56 - Thm("lin_isolate_div",num_str @{thm lin_isolate_div})
1.57 + Thm("lin_isolate_div",TermC.num_str @{thm lin_isolate_div})
1.58 (* bx=c -> x=c/b *)
1.59 ],
1.60 scr = EmptyScr}:rls);