1.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy.bak	Tue Sep 27 11:00:49 2011 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,65 +0,0 @@
     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 -
    1.18 -
    1.19 -*}
    1.20 -
    1.21 -
    1.22 -
    1.23 -subsection {*get the argument out of a fraction*}
    1.24 -
    1.25 -ML {*(*
    1.26 -(*("get_argument", ("Rational.get'_argument", eval_get_argument ""))*)
    1.27 -
    1.28 -
    1.29 -fun eval_get_argument "Atools.argument'_in" 
    1.30 -		     (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =
    1.31 -    if is_Free arg (*could be something to be simplified before*)
    1.32 -    then SOME (term2str t ^ " = " ^ term2str arg,
    1.33 -	       Trueprop $ (mk_equality (t, arg)))
    1.34 -    else NONE
    1.35 -  | eval_get_argument_in _ _ _ _ = NONE;
    1.36 -*)
    1.37 -*}
    1.38 -
    1.39 -
    1.40 -subsection {*store the function for fetching from script*}
    1.41 -
    1.42 -ML {*
    1.43 -calclist' := overwritel (!calclist',
    1.44 -  [
    1.45 -    ("get_denominator", ("Rational.get'_denominator", eval_get_denominator "")),
    1.46 -    ("get_argument", ("Rational.get'_argument", eval_get_argument ""))
    1.47 -  ]);
    1.48 -*}
    1.49 -
    1.50 -subsection{*rule set for partial fractions*}
    1.51 -ML {*
    1.52 -val partial_fraction = 
    1.53 -  Rls {id="partial_fraction", preconds = [], rew_ord = ("termlessI",termlessI), 
    1.54 -	  erls = Erls, srls = Erls, calc = [],
    1.55 -	  rules = [
    1.56 -				    Calc ("Rings.inverse_class.divide", eval_get_denominator "#", eval_get_argument "X")
    1.57 -		  ],
    1.58 -	 scr = EmptyScr};
    1.59 -*}
    1.60 -
    1.61 -subsection{*store the rule set for math engine*}
    1.62 -ML {*
    1.63 -  overwritelthy @{theory} (!ruleset', 
    1.64 -	    [("partial_fraction", prep_rls partial_fraction)
    1.65 -	     ]);
    1.66 -*}
    1.67 -
    1.68 -end
    1.69 \ No newline at end of file