1.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Tue Aug 31 15:36:57 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Tue Aug 31 16:00:13 2010 +0200
1.3 @@ -83,12 +83,12 @@
1.4 Calc ("Tools.rhs" ,eval_rhs ""),
1.5 Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
1.6 Calc ("op =",eval_equal "#equal_"),
1.7 - Thm ("not_true",num_str not_true),
1.8 - Thm ("not_false",num_str not_false),
1.9 - Thm ("and_true",num_str and_true),
1.10 - Thm ("and_false",num_str and_false),
1.11 - Thm ("or_true",num_str or_true),
1.12 - Thm ("or_false",num_str or_false)
1.13 + Thm ("not_true",num_str @{not_true),
1.14 + Thm ("not_false",num_str @{not_false),
1.15 + Thm ("and_true",num_str @{and_true),
1.16 + Thm ("and_false",num_str @{and_false),
1.17 + Thm ("or_true",num_str @{or_true),
1.18 + Thm ("or_false",num_str @{or_false)
1.19 ];
1.20
1.21
1.22 @@ -103,8 +103,8 @@
1.23 eval_is_ratequation_in "")
1.24
1.25 ]))
1.26 - [Thm ("and_commute",num_str and_commute), (*WN: ein Hack*)
1.27 - Thm ("or_commute",num_str or_commute) (*WN: ein Hack*)
1.28 + [Thm ("and_commute",num_str @{and_commute), (*WN: ein Hack*)
1.29 + Thm ("or_commute",num_str @{or_commute) (*WN: ein Hack*)
1.30 ];
1.31 ruleset' := overwritelthy thy (!ruleset',
1.32 [("rateq_erls",rateq_erls)(*FIXXXME:del with rls.rls'*)
1.33 @@ -120,8 +120,8 @@
1.34 Calc ("RatEq.is'_ratequation'_in",
1.35 eval_is_ratequation_in "")
1.36 ]))
1.37 - [Thm ("and_commute",num_str and_commute), (*WN: ein Hack*)
1.38 - Thm ("or_commute",num_str or_commute) (*WN: ein Hack*)
1.39 + [Thm ("and_commute",num_str @{and_commute), (*WN: ein Hack*)
1.40 + Thm ("or_commute",num_str @{or_commute) (*WN: ein Hack*)
1.41 ];
1.42
1.43 val RatEq_eliminate = prep_rls(
1.44 @@ -129,11 +129,11 @@
1.45 rew_ord = ("termlessI", termlessI), erls = rateq_erls, srls = Erls,
1.46 calc = [],
1.47 rules = [
1.48 - Thm("rat_mult_denominator_both",num_str rat_mult_denominator_both),
1.49 + Thm("rat_mult_denominator_both",num_str @{rat_mult_denominator_both),
1.50 (* a/b=c/d -> ad=cb *)
1.51 - Thm("rat_mult_denominator_left",num_str rat_mult_denominator_left),
1.52 + Thm("rat_mult_denominator_left",num_str @{rat_mult_denominator_left),
1.53 (* a =c/d -> ad=c *)
1.54 - Thm("rat_mult_denominator_right",num_str rat_mult_denominator_right)
1.55 + Thm("rat_mult_denominator_right",num_str @{rat_mult_denominator_right)
1.56 (* a/b=c -> a=cb *)
1.57 ],
1.58 scr = Script ((term_of o the o (parse thy)) "empty_script")
1.59 @@ -146,21 +146,21 @@
1.60 Rls {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI),
1.61 erls = rateq_erls, srls = Erls, calc = [],
1.62 rules = [
1.63 - Thm("real_rat_mult_1",num_str real_rat_mult_1),
1.64 + Thm("real_rat_mult_1",num_str @{real_rat_mult_1),
1.65 (*a*(b/c) = (a*b)/c*)
1.66 - Thm("real_rat_mult_2",num_str real_rat_mult_2),
1.67 + Thm("real_rat_mult_2",num_str @{real_rat_mult_2),
1.68 (*(a/b)*(c/d) = (a*c)/(b*d)*)
1.69 - Thm("real_rat_mult_3",num_str real_rat_mult_3),
1.70 + Thm("real_rat_mult_3",num_str @{real_rat_mult_3),
1.71 (* (a/b)*c = (a*c)/b*)
1.72 - Thm("real_rat_pow",num_str real_rat_pow),
1.73 + Thm("real_rat_pow",num_str @{real_rat_pow),
1.74 (*(a/b)^^^2 = a^^^2/b^^^2*)
1.75 - Thm("real_diff_minus",num_str real_diff_minus),
1.76 + Thm("real_diff_minus",num_str @{real_diff_minus),
1.77 (* a - b = a + (-1) * b *)
1.78 - Thm("rat_double_rat_1",num_str rat_double_rat_1),
1.79 + Thm("rat_double_rat_1",num_str @{rat_double_rat_1),
1.80 (* (a / (c/d) = (a*d) / c) *)
1.81 - Thm("rat_double_rat_2",num_str rat_double_rat_2),
1.82 + Thm("rat_double_rat_2",num_str @{rat_double_rat_2),
1.83 (* ((a/b) / (c/d) = (a*d) / (b*c)) *)
1.84 - Thm("rat_double_rat_3",num_str rat_double_rat_3)
1.85 + Thm("rat_double_rat_3",num_str @{rat_double_rat_3)
1.86 (* ((a/b) / c = a / (b*c) ) *)
1.87 ],
1.88 scr = Script ((term_of o the o (parse thy)) "empty_script")