1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Jun 21 14:39:52 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Jun 21 15:36:09 2021 +0200
     1.3 @@ -30,15 +30,15 @@
     1.4      ("is_atom", ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_")),
     1.5      ("is_even", ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_")),
     1.6      ("is_const", ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_")),
     1.7 -    ("le", ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")),
     1.8 -    ("leq", ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_")),
     1.9 +    ("le", (\<^const_name>\<open>less\<close>, Prog_Expr.eval_equ "#less_")),
    1.10 +    ("leq", (\<^const_name>\<open>less_eq\<close>, Prog_Expr.eval_equ "#less_equal_")),
    1.11      ("ident", ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")),
    1.12 -    ("equal", ("HOL.eq", Prog_Expr.eval_equal "#equal_")),
    1.13 -    ("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
    1.14 -    ("MINUS", ("Groups.minus_class.minus", (**)eval_binop "#sub_")),
    1.15 -    ("TIMES", ("Groups.times_class.times", (**)eval_binop "#mult_")),
    1.16 -    ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
    1.17 -    ("POWER",("Transcendental.powr", (**)eval_binop "#power_")),
    1.18 +    ("equal", (\<^const_name>\<open>HOL.eq\<close>, Prog_Expr.eval_equal "#equal_")),
    1.19 +    ("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
    1.20 +    ("MINUS", (\<^const_name>\<open>minus\<close>, (**)eval_binop "#sub_")),
    1.21 +    ("TIMES", (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
    1.22 +    ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
    1.23 +    ("POWER",(\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_")),
    1.24      ("boollist2sum", ("Prog_Expr.boollist2sum", Prog_Expr.eval_boollist2sum ""))]\<close>
    1.25  
    1.26  subsection \<open>rewrite-order for rule-sets\<close>