1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Nov 07 19:49:14 2022 +0100
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Nov 07 19:58:01 2022 +0100
     1.3 @@ -886,7 +886,7 @@
     1.4        with \em SignalProcessing \normalfont and go on by creating the node
     1.5        \em Z\_Transform\normalfont.\<close>
     1.6  
     1.7 -setup \<open>KEStore_Elems.add_pbls
     1.8 +setup \<open>Know_Store.add_pbls
     1.9    [Problem.prep_input @{theory} "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
    1.10      Problem.prep_input @{theory} "pbl_SP_Ztrans" [] Problem.id_empty
    1.11        (["Z_Transform", "SignalProcessing"], [], Rule_Set.empty, NONE, [])]\<close>
    1.12 @@ -895,7 +895,7 @@
    1.13         and output parameters. We already prepared their definition in
    1.14         Section~\ref{sec:deffdes}.\<close>
    1.15  
    1.16 -setup \<open>KEStore_Elems.add_pbls
    1.17 +setup \<open>Know_Store.add_pbls
    1.18    [Problem.prep_input @{theory} "pbl_SP_Ztrans_inv" [] Problem.id_empty
    1.19        (["Inverse", "Z_Transform", "SignalProcessing"],
    1.20          [("#Given" ,["filterExpression X_eq"]),
    1.21 @@ -924,7 +924,7 @@
    1.22        \normalfont node. We have to define both nodes first with an empty script
    1.23        as content.\<close>
    1.24  
    1.25 -setup \<open>KEStore_Elems.add_mets
    1.26 +setup \<open>Know_Store.add_mets
    1.27    [MethodC.prep_input @{theory} "met_SP" [] e_metID
    1.28        (["SignalProcessing"], [],
    1.29          {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
    1.30 @@ -941,7 +941,7 @@
    1.31        script we want to implement later. First we define the specifications
    1.32        of the script in e.g. the in- and output.\<close>
    1.33  
    1.34 -setup \<open>KEStore_Elems.add_mets
    1.35 +setup \<open>Know_Store.add_mets
    1.36    [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
    1.37        (["SignalProcessing", "Z_Transform", "Inverse"], 
    1.38          [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]),
    1.39 @@ -955,7 +955,7 @@
    1.40        script itself. As a first try we define only three rows containing one
    1.41        simple operation.\<close>
    1.42  
    1.43 -setup \<open>KEStore_Elems.add_mets
    1.44 +setup \<open>Know_Store.add_mets
    1.45    [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
    1.46        (["SignalProcessing", "Z_Transform", "Inverse"], 
    1.47          [("#Given" , ["filterExpression X_eq", "boundVariable X_z"]),
    1.48 @@ -1125,7 +1125,7 @@
    1.49        Note that we also did this stepwise, but we didn't kept every
    1.50        subversion.\<close>
    1.51  
    1.52 -setup \<open>KEStore_Elems.add_mets
    1.53 +setup \<open>Know_Store.add_mets
    1.54    [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
    1.55        (["SignalProcessing", "Z_Transform", "Inverse"], 
    1.56          [("#Given" , ["filterExpression X_eq"]), (*TODO boundVariable X_z*)