src/Tools/isac/Knowledge/Integrate.thy
changeset 60509 2e0b7ca391dc
parent 60504 8cc1415b3530
child 60515 03e19793d81e
     1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Wed Aug 03 18:17:27 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Thu Aug 04 12:48:37 2022 +0200
     1.3 @@ -158,12 +158,12 @@
     1.4  (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
     1.5  val norm_Rational_rls_noadd_fractions = 
     1.6    Rule_Def.Repeat {id = "norm_Rational_rls_noadd_fractions", preconds = [], 
     1.7 -    rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
     1.8 +    rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
     1.9      erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.10      rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*)
    1.11    	  Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
    1.12    		(Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], 
    1.13 -  		   rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
    1.14 +  		   rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
    1.15    		   erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
    1.16    				 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
    1.17    			 srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.18 @@ -187,7 +187,7 @@
    1.19  (*.for simplify_Integral adapted from 'norm_Rational'.*)
    1.20  val norm_Rational_noadd_fractions = 
    1.21    Rule_Set.Sequence {id = "norm_Rational_noadd_fractions", preconds = [], 
    1.22 -    rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
    1.23 +    rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
    1.24      erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.25      rules = [Rule.Rls_ discard_minus,
    1.26    		Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c    *)
    1.27 @@ -214,7 +214,7 @@
    1.28  		];
    1.29  val simplify_Integral = 
    1.30    Rule_Set.Sequence {id = "simplify_Integral", preconds = []:term list, 
    1.31 -    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
    1.32 +    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
    1.33      erls = Atools_erls, srls = Rule_Set.Empty,
    1.34      calc = [],  errpatts = [],
    1.35      rules = [