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 ;