1.1 --- a/src/sml/IsacKnowledge/Integrate.ML	Fri Jul 14 18:20:42 2006 +0200
     1.2 +++ b/src/sml/IsacKnowledge/Integrate.ML	Mon Jul 17 10:17:33 2006 +0200
     1.3 @@ -176,6 +176,20 @@
     1.4     This is a copy from 'make_ratpoly_in' with respective reduction of rules and
     1.5     *1* expand the term, ie. distribute * and / over +
     1.6  .*)
     1.7 +val separate_bdv2 =
     1.8 +    append_rls "separate_bdv2"
     1.9 +	       collect_bdv
    1.10 +	       [Thm ("separate_bdv", num_str separate_bdv),
    1.11 +		(*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
    1.12 +		Thm ("separate_bdv_n", num_str separate_bdv_n),
    1.13 +		Thm ("separate_1_bdv", num_str separate_1_bdv),
    1.14 +		(*"?bdv / ?b = (1 / ?b) * ?bdv"*)
    1.15 +		Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)(*,
    1.16 +			  (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
    1.17 +			  *****Thm ("real_add_divide_distrib", 
    1.18 +			  *****num_str real_add_divide_distrib)
    1.19 +			  (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
    1.20 +		];
    1.21  val simplify_Integral = 
    1.22    Seq {id = "simplify_Integral", preconds = []:term list, 
    1.23         rew_ord = ("dummy_ord", dummy_ord),
    1.24 @@ -190,19 +204,7 @@
    1.25  	       Rls_ order_add_mult_in,
    1.26  	       Rls_ discard_parentheses,
    1.27  	       (*Rls_ collect_bdv, from make_polynomial_in*)
    1.28 -	       Rls_ (append_rls "separate_bdv"
    1.29 -			 collect_bdv
    1.30 -			 [Thm ("separate_bdv", num_str separate_bdv),
    1.31 -			  (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
    1.32 -			  Thm ("separate_bdv_n", num_str separate_bdv_n),
    1.33 -			  Thm ("separate_1_bdv", num_str separate_1_bdv),
    1.34 -			  (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
    1.35 -			  Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)(*,
    1.36 -			  (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
    1.37 -			  *****Thm ("real_add_divide_distrib", 
    1.38 -			  *****num_str real_add_divide_distrib)
    1.39 -			  (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
    1.40 -			  ]),
    1.41 +	       Rls_ separate_bdv2,
    1.42  	       Calc ("HOL.divide"  ,eval_cancel "#divide_")
    1.43  	       ],
    1.44        scr = EmptyScr}:rls;      
    1.45 @@ -268,7 +270,12 @@
    1.46  	    [("integration_rules", prep_rls integration_rules),
    1.47  	     ("add_new_c", prep_rls add_new_c),
    1.48  	     ("simplify_Integral", prep_rls simplify_Integral),
    1.49 -	     ("integration", prep_rls integration)]);
    1.50 +	     ("integration", prep_rls integration),
    1.51 +	     ("separate_bdv2", separate_bdv2),
    1.52 +	     ("norm_Rational_noadd_fractions", norm_Rational_noadd_fractions),
    1.53 +	     ("norm_Rational_rls_noadd_fractions", 
    1.54 +	      norm_Rational_rls_noadd_fractions)
    1.55 +	     ]);
    1.56  
    1.57  (** problems **)
    1.58