1.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Tue Sep 27 11:00:49 2011 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Tue Sep 27 11:05:00 2011 +0200
     1.3 @@ -11,22 +11,42 @@
     1.4  	          Trueprop $ (mk_equality (t, denom)))
     1.5    | eval_get_denominator _ _ _ _ = NONE; 
     1.6  *}
     1.7 -text {*rule set for partial fractions*}
     1.8 +
     1.9 +
    1.10 +
    1.11 +subsection {*get the argument out of a fraction*}
    1.12 +
    1.13 +ML {*
    1.14 +(*("get_argument", ("Rational.get'_argument", eval_get_argument ""))*)
    1.15 +
    1.16 +(* 
    1.17 +fun eval_get_argument "Atools.argument'_in" 
    1.18 +		     (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =
    1.19 +    if is_Free arg (*could be something to be simplified before*)
    1.20 +    then SOME (term2str t ^ " = " ^ term2str arg,
    1.21 +	       Trueprop $ (mk_equality (t, arg)))
    1.22 +    else NONE
    1.23 +  | eval_argument_in _ _ _ _ = NONE;
    1.24 +*)
    1.25 +
    1.26 +*}
    1.27 +
    1.28 +subsection{*rule set for partial fractions*}
    1.29  ML {*
    1.30  val partial_fraction = 
    1.31    Rls {id="partial_fraction", preconds = [], rew_ord = ("termlessI",termlessI), 
    1.32  	  erls = Erls, srls = Erls, calc = [],
    1.33  	  rules = [
    1.34 -				    Calc ("Rings.inverse_class.divide", eval_get_denominator "#")
    1.35 +				    Calc ("Rings.inverse_class.divide", eval_get_denominator "#", eval_get_argument "X")
    1.36  		  ],
    1.37  	 scr = EmptyScr};
    1.38  *}
    1.39 -text {*store the rule set for math engine*}
    1.40 +
    1.41 +subsection{*store the rule set for math engine*}
    1.42  ML {*
    1.43    overwritelthy @{theory} (!ruleset', 
    1.44  	    [("partial_fraction", prep_rls partial_fraction)
    1.45  	     ]);
    1.46  *}
    1.47  
    1.48 -
    1.49  end
    1.50 \ No newline at end of file