1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Wed Apr 01 19:20:05 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Sat Apr 04 12:11:32 2020 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4  subsection \<open>rule-sets\<close>
     1.5  ML \<open>
     1.6  \<close> ML \<open>
     1.7 -val Atools_erls = Rule.append_rls "Atools_erls" Rule.e_rls
     1.8 +val Atools_erls = Rule_Set.append_rls "Atools_erls" Rule_Set.e_rls
     1.9    [ Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
    1.10      Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
    1.11  		(*"(~ True) = False"*)
    1.12 @@ -89,7 +89,7 @@
    1.13  \<close>
    1.14  
    1.15  ML \<open>
    1.16 -val Atools_crls = Rule.append_rls "Atools_crls" Rule.e_rls
    1.17 +val Atools_crls = Rule_Set.append_rls "Atools_crls" Rule_Set.e_rls
    1.18    [ Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
    1.19      Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
    1.20  		Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
    1.21 @@ -117,7 +117,7 @@
    1.22  subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
    1.23  text \<open>requires "eval_binop" from above\<close>
    1.24  ML \<open>
    1.25 -val prog_expr = Rule.append_rls "prog_expr" prog_expr
    1.26 +val prog_expr = Rule_Set.append_rls "prog_expr" prog_expr
    1.27  	[ Rule.Num_Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
    1.28  		Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), 
    1.29  		Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.30 @@ -130,15 +130,15 @@
    1.31  		Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
    1.32  		Rule.Thm ("if_False",TermC.num_str @{thm if_False})];
    1.33  
    1.34 -val prog_expr = Auto_Prog.prep_rls @{theory} (Rule.merge_rls "list_erls"
    1.35 -	(Rule.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
    1.36 -    erls = Rule.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), 
    1.37 -    erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
    1.38 +val prog_expr = Auto_Prog.prep_rls @{theory} (Rule_Set.merge_rls "list_erls"
    1.39 +	(Rule_Set.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
    1.40 +    erls = Rule_Set.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), 
    1.41 +    erls = Rule_Set.e_rls, srls = Rule_Set.Erls, calc = [], errpatts = [],
    1.42      rules = [Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
    1.43        Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")
    1.44        (*    ~~~~~~ for nth_Cons_*)],
    1.45      scr = Rule.EmptyScr},
    1.46 -    srls = Rule.Erls, calc = [], errpatts = [],
    1.47 +    srls = Rule_Set.Erls, calc = [], errpatts = [],
    1.48      rules = [], scr = Rule.EmptyScr})
    1.49    prog_expr);
    1.50  \<close>