1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed Feb 03 15:21:12 2021 +0100
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed Feb 03 16:39:44 2021 +0100
     1.3 @@ -513,7 +513,7 @@
     1.4        the original \emph{srls}.\\
     1.5  
     1.6  \begin{verbatim}
     1.7 -  val {srls,...} = Method.from_store ["SignalProcessing",
     1.8 +  val {srls,...} = MethodC.from_store ["SignalProcessing",
     1.9                              "Z_Transform",
    1.10                              "Inverse"];
    1.11  \end{verbatim}
    1.12 @@ -858,7 +858,7 @@
    1.13    if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";
    1.14  \<close>
    1.15  
    1.16 -section \<open>Implement the Specification and the Method \label{spec-meth}\<close>
    1.17 +section \<open>Implement the Specification and the MethodC \label{spec-meth}\<close>
    1.18  
    1.19  text\<open>\noindent Now everything we need for solving the problem has been
    1.20        tested out. We now start by creating new nodes for our methods and
    1.21 @@ -904,7 +904,7 @@
    1.22    Problem.from_store ["Inverse", "Z_Transform", "SignalProcessing"];
    1.23  \<close>
    1.24  
    1.25 -subsection \<open>Define Name and Signature for the Method\<close>
    1.26 +subsection \<open>Define Name and Signature for the MethodC\<close>
    1.27  
    1.28  text\<open>\noindent As a next step we store the definition of our new method as a
    1.29        constant for the interpreter.\<close>
    1.30 @@ -913,7 +913,7 @@
    1.31    InverseZTransform :: "[bool, bool] => bool"
    1.32      ("((Program InverseZTransform (_ =))// (_))" 9)
    1.33  
    1.34 -subsection \<open>Setup Parent Nodes in Hierarchy of Method\label{sec:cparentnode}\<close>
    1.35 +subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\label{sec:cparentnode}\<close>
    1.36  
    1.37  text\<open>\noindent Again we have to generate the nodes step by step, first the
    1.38        parent node and then the originally \em Z\_Transformation 
    1.39 @@ -921,12 +921,12 @@
    1.40        as content.\<close>
    1.41  
    1.42  setup \<open>KEStore_Elems.add_mets
    1.43 -  [Method.prep_input thy "met_SP" [] e_metID
    1.44 +  [MethodC.prep_input thy "met_SP" [] e_metID
    1.45        (["SignalProcessing"], [],
    1.46          {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
    1.47            errpats = [], nrls = Rule_Set.empty},
    1.48          "empty_script"),
    1.49 -    Method.prep_input thy "met_SP_Ztrans" [] e_metID
    1.50 +    MethodC.prep_input thy "met_SP_Ztrans" [] e_metID
    1.51        (["SignalProcessing", "Z_Transform"], [],
    1.52          {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
    1.53            errpats = [], nrls = Rule_Set.empty},
    1.54 @@ -938,7 +938,7 @@
    1.55        of the script in e.g. the in- and output.\<close>
    1.56  
    1.57  setup \<open>KEStore_Elems.add_mets
    1.58 -  [Method.prep_input thy "met_SP_Ztrans_inv" [] e_metID
    1.59 +  [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
    1.60        (["SignalProcessing", "Z_Transform", "Inverse"], 
    1.61          [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]),
    1.62            ("#Find", ["stepResponse n_eq"])],
    1.63 @@ -952,7 +952,7 @@
    1.64        simple operation.\<close>
    1.65  
    1.66  setup \<open>KEStore_Elems.add_mets
    1.67 -  [Method.prep_input thy "met_SP_Ztrans_inv" [] e_metID
    1.68 +  [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
    1.69        (["SignalProcessing", "Z_Transform", "Inverse"], 
    1.70          [("#Given" , ["filterExpression X_eq", "boundVariable X_z"]),
    1.71            ("#Find", ["stepResponse n_eq"])],
    1.72 @@ -974,7 +974,7 @@
    1.73        the hierarchy.\<close>
    1.74  
    1.75  ML \<open>
    1.76 -  Method.from_store ["SignalProcessing", "Z_Transform", "Inverse"];
    1.77 +  MethodC.from_store ["SignalProcessing", "Z_Transform", "Inverse"];
    1.78  \<close>
    1.79  
    1.80  section \<open>Program in TP-based language \label{prog-steps}\<close>
    1.81 @@ -1122,7 +1122,7 @@
    1.82        subversion.\<close>
    1.83  
    1.84  setup \<open>KEStore_Elems.add_mets
    1.85 -  [Method.prep_input thy "met_SP_Ztrans_inv" [] e_metID
    1.86 +  [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
    1.87        (["SignalProcessing", "Z_Transform", "Inverse"], 
    1.88          [("#Given" , ["filterExpression X_eq"]), (*TODO boundVariable X_z*)
    1.89            ("#Find", ["stepResponse n_eq"])],
    1.90 @@ -1231,7 +1231,7 @@
    1.91        ) = O_Model.init fmz thy ((#ppc o Problem.from_store) pI);
    1.92  
    1.93    val Prog sc 
    1.94 -    = (#scr o Method.from_store) ["SignalProcessing",
    1.95 +    = (#scr o MethodC.from_store) ["SignalProcessing",
    1.96                          "Z_Transform",
    1.97                          "Inverse"];
    1.98    atomty sc;
    1.99 @@ -1307,7 +1307,7 @@
   1.100           arguments in the arguments\ldots
   1.101           \begin{verbatim}
   1.102       val Prog s =
   1.103 -     (#scr o Method.from_store) ["SignalProcessing",
   1.104 +     (#scr o MethodC.from_store) ["SignalProcessing",
   1.105                         "Z_Transform",
   1.106                         "Inverse"];
   1.107       writeln (UnparseC.term s);
   1.108 @@ -1591,7 +1591,7 @@
   1.109          parse-tree of the program with {\sisac}'s specific debug tools:
   1.110        \begin{verbatim}
   1.111        val {scr = Prog t,...} = 
   1.112 -        Method.from_store ["simplification",
   1.113 +        MethodC.from_store ["simplification",
   1.114                   "of_rationals",
   1.115                   "to_partial_fraction"];
   1.116        atomty_thy @{theory "Inverse_Z_Transform"} t ;