1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Jun 09 20:28:42 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Thu Jun 10 11:54:20 2021 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5  theory Know_Store
     1.6    imports Complex_Main
     1.7 -  keywords "setup_rule" :: thy_decl
     1.8 +  keywords "rule_set_knowledge" :: thy_decl
     1.9  begin
    1.10  
    1.11  setup \<open>
    1.12 @@ -188,7 +188,7 @@
    1.13      flat (separate (ml ",") (map (ml_rule thy) args)) @ ml "])";
    1.14  
    1.15  val _ =
    1.16 -  Outer_Syntax.command \<^command_keyword>\<open>setup_rule\<close> "setup ISAC rules"
    1.17 +  Outer_Syntax.command \<^command_keyword>\<open>rule_set_knowledge\<close> "register ISAC rule set to Knowledge Store"
    1.18      (Parse.and_list1 parse_rule >> (fn args => Toplevel.theory (fn thy =>
    1.19        thy |> Context.theory_map
    1.20          (ML_Context.expression (Position.thread_data ()) (ml_rules thy args)))));
    1.21 @@ -238,7 +238,7 @@
    1.22  fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
    1.23  \<close>
    1.24  
    1.25 -setup_rule
    1.26 +rule_set_knowledge
    1.27    empty = \<open>Rule_Set.empty\<close> and
    1.28    e_rrls = \<open>Rule_Set.e_rrls\<close>
    1.29