1.1 --- a/test/Tools/isac/Knowledge/rational-2.sml	Mon Aug 02 15:30:41 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml	Tue Aug 03 19:16:27 2021 +0200
     1.3 @@ -17,7 +17,6 @@
     1.4  "Rfuns-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
     1.5  "----------- rewrite_set_ Partial_Fractions norm_Rational --------------------------------------";
     1.6  "----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";
     1.7 -"----------- fun cancel_p with Const AA --------------------------------------------------------";
     1.8  "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
     1.9  "-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";
    1.10  "-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";
    1.11 @@ -457,31 +456,7 @@
    1.12    if c = 1 andalso id = "Partial_Fractions.AA"
    1.13    then () else error "monom_of_term Const changed 1"
    1.14  | _ => error "monom_of_term Const changed 2";
    1.15 -
    1.16 -"----------- fun cancel_p with Const AA --------------------------------------------------------";
    1.17 -"----------- fun cancel_p with Const AA --------------------------------------------------------";
    1.18 -"----------- fun cancel_p with Const AA --------------------------------------------------------";
    1.19 -val thy = @{theory Partial_Fractions};
    1.20 -val ctxt = Proof_Context.init_global @{theory}
    1.21 -val SOME t = TermC.parseNEW ctxt "2 * AA / 2"; (* Const (\<^const_name>\<open>AA\<close>, "real") *)
    1.22 -
    1.23 -val SOME (t', _) = rewrite_set_ thy true cancel_p t;
    1.24 -case t' of
    1.25 -  Const (\<^const_name>\<open>divide\<close>, _) $ Const (\<^const_name>\<open>AA\<close>, _) $
    1.26 -    Const (\<^const_name>\<open>one_class.one\<close>, _) => ()
    1.27 -| _ => error "WRONG rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA changed";
    1.28 -
    1.29 -"~~~~~ fun cancel_p , args:"; val (t) = (t);
    1.30 -val opt = check_fraction t
    1.31 -val SOME (numerator, denominator) = (*case*) opt (*of*);
    1.32 -
    1.33 -if UnparseC.term numerator = "2 * AA" andalso UnparseC.term denominator = "2"
    1.34 -then () else error "check_fraction (2 * AA / 2) changed";
    1.35 -        val vs = TermC.vars_of t;
    1.36 -case vs of
    1.37 -  [Const (\<^const_name>\<open>AA\<close>, _)] => ()
    1.38 -| _ => error "rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA/1  changed";
    1.39 -
    1.40 +                                                  
    1.41  
    1.42  "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
    1.43  "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";