1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Tue Jun 01 15:41:23 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Sat Jul 03 16:21:07 2021 +0200
     1.3 @@ -123,20 +123,20 @@
     1.4  ML \<open>
     1.5  fun monom_of_term vs (c, es) (t as Const _) =
     1.6      (c, list_update es (find_index (curry op = t) vs) 1)
     1.7 -  | monom_of_term  vs (c, es) (t as (Const ("Num.numeral_class.numeral", _) $ _)) =
     1.8 -    if TermC.is_num t
     1.9 -    then (t |> HOLogic.dest_number |> snd |> string_of_int
    1.10 +  | monom_of_term vs (c, es) (t as (Const ("Num.numeral_class.numeral", _) $ _)) =
    1.11 +    (t |> HOLogic.dest_number |> snd |> string_of_int
    1.12        |> TermC.int_opt_of_string |> the |> curry op * c, es) (*several numerals in one monom*)
    1.13 -    else (c, list_update es (find_index (curry op = t) vs) 1)
    1.14 -  | monom_of_term  vs (c, es) (Const ("Transcendental.powr", _) $
    1.15 -      (t as (Const ("Num.numeral_class.numeral", _) $ _)) $
    1.16 -        (Const ("Num.numeral_class.numeral", _) $ num)) =
    1.17 +  | monom_of_term  vs (c, es) (t as Free _) =
    1.18 +    (c, list_update es (find_index (curry op = t) vs) 1)
    1.19 +  | monom_of_term  vs (c, es) (Const ("Transcendental.powr", _) $ (t as Free _) $
    1.20 +      (Const ("Num.numeral_class.numeral", _) $ num)) =
    1.21      (c, list_update es (find_index (curry op = t) vs) (num |> HOLogic.dest_numeral))
    1.22    | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
    1.23      let val (c', es') = monom_of_term vs (c, es) m1
    1.24      in monom_of_term vs (c', es') m2 end
    1.25    | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term t)
    1.26  
    1.27 +(*-------v------*)
    1.28  fun monoms_of_term vs (t as Const _) =
    1.29      [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.30    | monoms_of_term vs (t as Free _) =
    1.31 @@ -604,19 +604,6 @@
    1.32  
    1.33  section \<open>Rulesets for general simplification\<close>
    1.34  ML \<open>
    1.35 -(*erls for calculate_Rational; make local with FIXX@ME result:term *term list*)
    1.36 -val powers_erls = prep_rls'(
    1.37 -  Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
    1.38 -      erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.39 -      rules = [Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"),
    1.40 -	       Rule.Eval ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_"),
    1.41 -	       Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.42 -	       Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
    1.43 -	       Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
    1.44 -	       Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
    1.45 -	       ],
    1.46 -      scr = Rule.Empty_Prog
    1.47 -      });
    1.48  (*.all powers over + distributed; atoms over * collected, other distributed
    1.49     contains absolute minimum of thms for context in norm_Rational .*)
    1.50  val powers = prep_rls'(