1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Wed May 26 16:19:41 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Wed May 26 16:24:05 2021 +0200
     1.3 @@ -64,8 +64,7 @@
     1.4       *)
     1.5      ];
     1.6  \<close>
     1.7 -setup \<open>KEStore_Elems.add_rlss 
     1.8 -  [("LinEq_erls", (Context.theory_name @{theory}, LinEq_erls))]\<close>
     1.9 +setup_rule LinEq_erls = LinEq_erls
    1.10  ML \<open>
    1.11      
    1.12  val LinPoly_simplify = prep_rls'(
    1.13 @@ -87,8 +86,7 @@
    1.14  		],
    1.15         scr = Rule.Empty_Prog});
    1.16  \<close>
    1.17 -setup \<open>KEStore_Elems.add_rlss 
    1.18 -  [("LinPoly_simplify", (Context.theory_name @{theory}, LinPoly_simplify))]\<close>
    1.19 +setup_rule LinPoly_simplify = LinPoly_simplify
    1.20  ML \<open>
    1.21  
    1.22  (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
    1.23 @@ -108,8 +106,7 @@
    1.24  	      ],
    1.25       scr = Rule.Empty_Prog});
    1.26  \<close>
    1.27 -setup \<open>KEStore_Elems.add_rlss 
    1.28 -  [("LinEq_simplify", (Context.theory_name @{theory}, LinEq_simplify))]\<close>
    1.29 +setup_rule LinEq_simplify = LinEq_simplify
    1.30  
    1.31  (*----------------------------- problem types --------------------------------*)
    1.32  (* ---------linear----------- *)