src/Tools/isac/Knowledge/Integrate.thy
changeset 52105 2786cc9704c8
parent 52062 b3f18f0d55d9
child 52125 6f1d3415dc68
equal deleted inserted replaced
52104:83166e7c7e52 52105:2786cc9704c8
   173 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
   173 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
   174 val norm_Rational_rls_noadd_fractions = 
   174 val norm_Rational_rls_noadd_fractions = 
   175 Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [], 
   175 Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [], 
   176      rew_ord = ("dummy_ord",dummy_ord), 
   176      rew_ord = ("dummy_ord",dummy_ord), 
   177      erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [],
   177      erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [],
   178      rules = [(*Rls_ common_nominator_p_rls,!!!*)
   178      rules = [(*Rls_ add_fractions_p_rls,!!!*)
   179 	      Rls_ (*rat_mult_div_pow original corrected WN051028*)
   179 	      Rls_ (*rat_mult_div_pow original corrected WN051028*)
   180 		  (Rls {id = "rat_mult_div_pow", preconds = [], 
   180 		  (Rls {id = "rat_mult_div_pow", preconds = [], 
   181 		       rew_ord = ("dummy_ord",dummy_ord), 
   181 		       rew_ord = ("dummy_ord",dummy_ord), 
   182 		       erls = (*FIXME.WN051028 e_rls,*)
   182 		       erls = (*FIXME.WN051028 e_rls,*)
   183 		       append_rls "e_rls-is_polyexp" e_rls
   183 		       append_rls "e_rls-is_polyexp" e_rls