1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Sun Feb 09 16:21:26 2020 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Sun Feb 09 16:55:41 2020 +0100
     1.3 @@ -117,7 +117,7 @@
     1.4  subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
     1.5  text \<open>requires "eval_binop" from above\<close>
     1.6  ML \<open>
     1.7 -val list_rls = Rule.append_rls "list_rls" list_rls
     1.8 +val prog_expr = Rule.append_rls "prog_expr" prog_expr
     1.9  	[ Rule.Num_Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
    1.10  		Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), 
    1.11  		Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.12 @@ -130,7 +130,7 @@
    1.13  		Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
    1.14  		Rule.Thm ("if_False",TermC.num_str @{thm if_False})];
    1.15  
    1.16 -val list_rls = Auto_Prog.prep_rls @{theory} (Rule.merge_rls "list_erls"
    1.17 +val prog_expr = Auto_Prog.prep_rls @{theory} (Rule.merge_rls "list_erls"
    1.18  	(Rule.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
    1.19      erls = Rule.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), 
    1.20      erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
    1.21 @@ -140,10 +140,10 @@
    1.22      scr = Rule.EmptyScr},
    1.23      srls = Rule.Erls, calc = [], errpatts = [],
    1.24      rules = [], scr = Rule.EmptyScr})
    1.25 -  list_rls);
    1.26 +  prog_expr);
    1.27  \<close>
    1.28  subsection \<open>setup for extended rule-set\<close>
    1.29  setup \<open>KEStore_Elems.add_rlss
    1.30 -  [("list_rls", (Context.theory_name @{theory}, Auto_Prog.prep_rls @{theory} list_rls))]\<close>
    1.31 +  [("prog_expr", (Context.theory_name @{theory}, Auto_Prog.prep_rls @{theory} prog_expr))]\<close>
    1.32  
    1.33  end
    1.34 \ No newline at end of file