1.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Wed Sep 08 12:41:04 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Wed Sep 08 16:28:24 2010 +0200
     1.3 @@ -68,7 +68,8 @@
     1.4      else SOME ((term2str p) ^ " = True",
     1.5  	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
     1.6    | eval_is_rootRatAddTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
     1.7 -
     1.8 +*}
     1.9 +ML {*
    1.10  (*-------------------------rulse-------------------------*)
    1.11  val RootRatEq_prls = 
    1.12      append_rls "RootRatEq_prls" e_rls
    1.13 @@ -105,27 +106,31 @@
    1.14  ruleset' := overwritelthy @{theory} (!ruleset',
    1.15  	     [("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*)]);
    1.16  
    1.17 +*}
    1.18 +ML {*
    1.19  (* Solves a rootrat Equation *)
    1.20   val rootrat_solve = prep_rls(
    1.21       Rls {id = "rootrat_solve", preconds = [], 
    1.22  	  rew_ord = ("termlessI",termlessI), 
    1.23       erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
    1.24 -     rules = [Thm("rootrat_equation_left_1", num_str @{thm }rootrat_equation_left_1),   
    1.25 +     rules = 
    1.26 +     [Thm("rootrat_equation_left_1", num_str @{thm rootrat_equation_left_1}),   
    1.27  	        (* [|c is_rootTerm_in bdv|] ==> 
    1.28                                      ( (a + b/c = d) = ( b = (d - a) * c )) *)
    1.29 -              Thm("rootrat_equation_left_2",num_str @{thm rootrat_equation_left_2}),
    1.30 +      Thm("rootrat_equation_left_2",num_str @{thm rootrat_equation_left_2}),
    1.31  	        (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *)
    1.32 -	      Thm("rootrat_equation_right_1",num_str @{thm rootrat_equation_right_1}),
    1.33 +      Thm("rootrat_equation_right_1",num_str @{thm rootrat_equation_right_1}),
    1.34  		(* [|f is_rootTerm_in bdv|] ==> 
    1.35                                      ( (a = d + e/f) = ( (a - d) * f = e )) *)
    1.36 -	      Thm("rootrat_equation_right_2",num_str @{thm rootrat_equation_right_2})
    1.37 +      Thm("rootrat_equation_right_2",num_str @{thm rootrat_equation_right_2})
    1.38  		(* [|f is_rootTerm_in bdv|] ==> ( (a =  e/f) = ( a  * f = e ))*)
    1.39 -	      ],
    1.40 -	 scr = Script ((term_of o the o (parse thy)) "empty_script")
    1.41 -         }:rls);
    1.42 +      ], scr = Script ((term_of o the o (parse thy)) "empty_script")}:rls);
    1.43 +
    1.44  ruleset' := overwritelthy @{theory} (!ruleset',
    1.45  			[("rootrat_solve",rootrat_solve)
    1.46  			 ]);
    1.47 +*}
    1.48 +ML {*
    1.49  
    1.50  (*-----------------------probleme------------------------*)
    1.51  (*
    1.52 @@ -143,7 +148,8 @@
    1.53     ],
    1.54    RootRatEq_prls, SOME "solve (e_e::bool, v_v)",
    1.55    [["RootRatEq","elim_rootrat_equation"]]));
    1.56 -
    1.57 +*}
    1.58 +ML {*
    1.59  (*-------------------------Methode-----------------------*)
    1.60  store_met
    1.61   (prep_met (theory "LinEq") "met_rootrateq" [] e_metID
    1.62 @@ -173,10 +179,10 @@
    1.63      "           (Try (Rewrite_Set rooteq_simplify   False)) @@  " ^ 
    1.64      "           (Try (Rewrite_Set make_rooteq       False)) @@  " ^
    1.65      "           (Try (Rewrite_Set rooteq_simplify   False)) @@  " ^
    1.66 -    "           (Try (Rewrite_Set_Inst [(bdv,v_)]               " ^
    1.67 +    "           (Try (Rewrite_Set_Inst [(bdv,v_v)]               " ^
    1.68      "                                  rootrat_solve False))) e_e " ^
    1.69      " in (SubProblem (RootEq',[univariate,equation],            " ^
    1.70 -    "        [no_met]) [BOOL e_e, REAL v_]))"
    1.71 +    "        [no_met]) [BOOL e_e, REAL v_v]))"
    1.72     ));
    1.73  calclist':= overwritel (!calclist', 
    1.74     [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in",