1.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Tue Sep 28 10:01:18 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Tue Sep 28 10:10:26 2010 +0200
1.3 @@ -116,17 +116,17 @@
1.4 let val s::ss = explode str
1.5 in implode ((chr (ord s + 1))::ss) end;
1.6 fun identifier (Free (id,_)) = id (* 2, a *)
1.7 - | identifier (Const ("op *", _) $ Free (num, _) $ Free (id, _)) =
1.8 + | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) =
1.9 id (* 2*a, a*b *)
1.10 - | identifier (Const ("op *", _) $ (* 3*a*b *)
1.11 - (Const ("op *", _) $
1.12 + | identifier (Const ("Groups.times_class.times", _) $ (* 3*a*b *)
1.13 + (Const ("Groups.times_class.times", _) $
1.14 Free (num, _) $ Free _) $ Free (id, _)) =
1.15 if is_numeral num then id
1.16 else "|||||||||||||"
1.17 | identifier (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =
1.18 if is_numeral base then "|||||||||||||" (* a^2 *)
1.19 else (*increase*) base
1.20 - | identifier (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *)
1.21 + | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *)
1.22 (Const ("Atools.pow", _) $
1.23 Free (base, _) $ Free (exp, _))) =
1.24 if is_numeral num andalso not (is_numeral base) then (*increase*) base
1.25 @@ -155,20 +155,20 @@
1.26 | eval_kleiner _ _ _ _ = NONE;
1.27
1.28 fun ist_monom (Free (id,_)) = true
1.29 - | ist_monom (Const ("op *", _) $ Free (num, _) $ Free (id, _)) =
1.30 + | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) =
1.31 if is_numeral num then true else false
1.32 | ist_monom _ = false;
1.33 (*. this function only accepts the most simple monoms vvvvvvvvvv .*)
1.34 fun ist_monom (Free (id,_)) = true (* 2, a *)
1.35 - | ist_monom (Const ("op *", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *)
1.36 + | ist_monom (Const ("Groups.times_class.times", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *)
1.37 if is_numeral id then false else true
1.38 - | ist_monom (Const ("op *", _) $ (* 3*a*b *)
1.39 - (Const ("op *", _) $
1.40 + | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a*b *)
1.41 + (Const ("Groups.times_class.times", _) $
1.42 Free (num, _) $ Free _) $ Free (id, _)) =
1.43 if is_numeral num andalso not (is_numeral id) then true else false
1.44 | ist_monom (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =
1.45 true (* a^2 *)
1.46 - | ist_monom (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *)
1.47 + | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *)
1.48 (Const ("Atools.pow", _) $
1.49 Free (base, _) $ Free (exp, _))) =
1.50 if is_numeral num then true else false
1.51 @@ -297,7 +297,7 @@
1.52 Thm ("vorzeichen_minus_weg4",num_str @{thm vorzeichen_minus_weg4}),
1.53 (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
1.54
1.55 - Calc ("op *", eval_binop "#mult_"),
1.56 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.57
1.58 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
1.59 (*"0 * z = 0"*)
1.60 @@ -381,7 +381,7 @@
1.61 ];
1.62 val rechnen =
1.63 append_rls "rechnen" e_rls
1.64 - [Calc ("op *", eval_binop "#mult_"),
1.65 + [Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.66 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.67 Calc ("Groups.minus_class.minus", eval_binop "#subtr_")
1.68 ];