1.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Tue Aug 31 15:36:57 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Tue Aug 31 16:00:13 2010 +0200
1.3 @@ -78,12 +78,12 @@
1.4 Calc ("RootRatEq.is'_rootRatAddTerm'_in",
1.5 eval_is_rootRatAddTerm_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 val RooRatEq_erls =
1.22 @@ -108,15 +108,15 @@
1.23 Rls {id = "rootrat_solve", preconds = [],
1.24 rew_ord = ("termlessI",termlessI),
1.25 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
1.26 - rules = [Thm("rootrat_equation_left_1", num_str rootrat_equation_left_1),
1.27 + rules = [Thm("rootrat_equation_left_1", num_str @{rootrat_equation_left_1),
1.28 (* [|c is_rootTerm_in bdv|] ==>
1.29 ( (a + b/c = d) = ( b = (d - a) * c )) *)
1.30 - Thm("rootrat_equation_left_2",num_str rootrat_equation_left_2),
1.31 + Thm("rootrat_equation_left_2",num_str @{rootrat_equation_left_2),
1.32 (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *)
1.33 - Thm("rootrat_equation_right_1",num_str rootrat_equation_right_1),
1.34 + Thm("rootrat_equation_right_1",num_str @{rootrat_equation_right_1),
1.35 (* [|f is_rootTerm_in bdv|] ==>
1.36 ( (a = d + e/f) = ( (a - d) * f = e )) *)
1.37 - Thm("rootrat_equation_right_2",num_str rootrat_equation_right_2)
1.38 + Thm("rootrat_equation_right_2",num_str @{rootrat_equation_right_2)
1.39 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*)
1.40 ],
1.41 scr = Script ((term_of o the o (parse thy)) "empty_script")