1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Wed Jun 09 20:28:42 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Thu Jun 10 11:54:20 2021 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4       *)
     1.5      ];
     1.6  \<close>
     1.7 -setup_rule LinEq_erls = LinEq_erls
     1.8 +rule_set_knowledge LinEq_erls = LinEq_erls
     1.9  ML \<open>
    1.10      
    1.11  val LinPoly_simplify = prep_rls'(
    1.12 @@ -86,7 +86,7 @@
    1.13  		],
    1.14         scr = Rule.Empty_Prog});
    1.15  \<close>
    1.16 -setup_rule LinPoly_simplify = LinPoly_simplify
    1.17 +rule_set_knowledge LinPoly_simplify = LinPoly_simplify
    1.18  ML \<open>
    1.19  
    1.20  (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
    1.21 @@ -106,7 +106,7 @@
    1.22  	      ],
    1.23       scr = Rule.Empty_Prog});
    1.24  \<close>
    1.25 -setup_rule LinEq_simplify = LinEq_simplify
    1.26 +rule_set_knowledge LinEq_simplify = LinEq_simplify
    1.27  
    1.28  (*----------------------------- problem types --------------------------------*)
    1.29  (* ---------linear----------- *)