test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy
changeset 59970 ab1c25c0339a
parent 59965 0763aec4c5b6
child 59971 2909d58a5c5d
     1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Tue May 12 16:22:00 2020 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Tue May 12 17:42:29 2020 +0200
     1.3 @@ -266,7 +266,7 @@
     1.4  text \<open>\noindent Check if the given equation matches the specification of this
     1.5          equation type.\<close>
     1.6  ML \<open>
     1.7 -  Specify.match_pbl fmz (Specify.get_pbt ["univariate","equation"]);
     1.8 +  Specify.match_pbl fmz (Problem.from_store ["univariate","equation"]);
     1.9  \<close>
    1.10  
    1.11  text\<open>\noindent We switch up to the {\sisac} Context and try to solve the 
    1.12 @@ -290,7 +290,7 @@
    1.13          specification of this equation type.\<close>
    1.14          
    1.15  ML \<open>
    1.16 -  Specify.match_pbl fmz (Specify.get_pbt
    1.17 +  Specify.match_pbl fmz (Problem.from_store
    1.18      ["abcFormula","degree_2","polynomial","univariate","equation"]);
    1.19  \<close>
    1.20  
    1.21 @@ -513,7 +513,7 @@
    1.22        the original \emph{srls}.\\
    1.23  
    1.24  \begin{verbatim}
    1.25 -  val {srls,...} = get_met ["SignalProcessing",
    1.26 +  val {srls,...} = Method.from_store ["SignalProcessing",
    1.27                              "Z_Transform",
    1.28                              "Inverse"];
    1.29  \end{verbatim}
    1.30 @@ -901,7 +901,7 @@
    1.31          [["SignalProcessing","Z_Transform","Inverse"]])]\<close>
    1.32  ML \<open>
    1.33    Specify.show_ptyps() ();
    1.34 -  get_pbt ["Inverse","Z_Transform","SignalProcessing"];
    1.35 +  Problem.from_store ["Inverse","Z_Transform","SignalProcessing"];
    1.36  \<close>
    1.37  
    1.38  subsection \<open>Define Name and Signature for the Method\<close>
    1.39 @@ -974,7 +974,7 @@
    1.40        the hierarchy.\<close>
    1.41  
    1.42  ML \<open>
    1.43 -  get_met ["SignalProcessing","Z_Transform","Inverse"];
    1.44 +  Method.from_store ["SignalProcessing","Z_Transform","Inverse"];
    1.45  \<close>
    1.46  
    1.47  section \<open>Program in TP-based language \label{prog-steps}\<close>
    1.48 @@ -1228,10 +1228,10 @@
    1.49              [Free ("x", _) $ _]
    1.50            )
    1.51         ],_
    1.52 -      ) = O_Model.init fmz thy ((#ppc o get_pbt) pI);
    1.53 +      ) = O_Model.init fmz thy ((#ppc o Problem.from_store) pI);
    1.54  
    1.55    val Prog sc 
    1.56 -    = (#scr o get_met) ["SignalProcessing",
    1.57 +    = (#scr o Method.from_store) ["SignalProcessing",
    1.58                          "Z_Transform",
    1.59                          "Inverse"];
    1.60    atomty sc;
    1.61 @@ -1307,7 +1307,7 @@
    1.62           arguments in the arguments\ldots
    1.63           \begin{verbatim}
    1.64       val Prog s =
    1.65 -     (#scr o get_met) ["SignalProcessing",
    1.66 +     (#scr o Method.from_store) ["SignalProcessing",
    1.67                         "Z_Transform",
    1.68                         "Inverse"];
    1.69       writeln (UnparseC.term s);
    1.70 @@ -1591,7 +1591,7 @@
    1.71          parse-tree of the program with {\sisac}'s specific debug tools:
    1.72        \begin{verbatim}
    1.73        val {scr = Prog t,...} = 
    1.74 -        get_met ["simplification",
    1.75 +        Method.from_store ["simplification",
    1.76                   "of_rationals",
    1.77                   "to_partial_fraction"];
    1.78        atomty_thy @{theory "Inverse_Z_Transform"} t ;