1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Fri Sep 23 16:22:11 2011 +0200
     1.3 @@ -0,0 +1,32 @@
     1.4 +theory Partial_Fractions imports Rational begin
     1.5 +
     1.6 +subsection {*get the denominator out of a fraction*}
     1.7 +text {*this function can be put into rule sets*}
     1.8 +ML {*
     1.9 +(*("get_denominator", ("Rational.get'_denominator", eval_get_denominator ""))*)
    1.10 +fun eval_get_denominator (thmid:string) _ 
    1.11 +		      (t as (Const("Rings.inverse_class.divide", _) $ num $ denom)) thy = 
    1.12 +    SOME (mk_thmid thmid "" 
    1.13 +            (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "", 
    1.14 +	          Trueprop $ (mk_equality (t, denom)))
    1.15 +  | eval_get_denominator _ _ _ _ = NONE; 
    1.16 +*}
    1.17 +text {*rule set for partial fractions*}
    1.18 +ML {*
    1.19 +val partial_fraction = 
    1.20 +  Rls {id="partial_fraction", preconds = [], rew_ord = ("termlessI",termlessI), 
    1.21 +	  erls = Erls, srls = Erls, calc = [],
    1.22 +	  rules = [
    1.23 +				    Calc ("Rings.inverse_class.divide", eval_get_denominator "#")
    1.24 +		  ],
    1.25 +	 scr = EmptyScr};
    1.26 +*}
    1.27 +text {*store the rule set for math engine*}
    1.28 +ML {*
    1.29 +  overwritelthy @{theory} (!ruleset', 
    1.30 +	    [("partial_fraction", prep_rls partial_fraction)
    1.31 +	     ]);
    1.32 +*}
    1.33 +
    1.34 +
    1.35 +end
    1.36 \ No newline at end of file