1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Aug 22 15:56:48 2019 +0200
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Aug 22 16:48:04 2019 +0200
1.3 @@ -186,7 +186,7 @@
1.4
1.5 text\<open>\noindent We have rhs\footnote{Note: lhs means \em Left Hand Side
1.6 \normalfont and rhs means \em Right Hand Side \normalfont and indicates
1.7 - the left or the right part of an equation.} in the Script language, but
1.8 + the left or the right part of an equation.} in the Program language, but
1.9 we need a function which gets the denominator of a fraction.\<close>
1.10
1.11 subsubsection\<open>Get the Denominator and Numerator out of a Fraction\<close>
1.12 @@ -198,7 +198,7 @@
1.13 get_numerator :: "real => real"
1.14
1.15 text \<open>\noindent With the above definition we run into problems when we parse
1.16 - the Script \texttt{InverseZTransform}. This leads to \em ambiguous
1.17 + the Program \texttt{InverseZTransform}. This leads to \em ambiguous
1.18 parse trees. \normalfont We avoid this by moving the definition
1.19 to \ttfamily Rational.thy \normalfont and re-building {\sisac}.
1.20 \par \noindent ATTENTION: From now on \ttfamily
1.21 @@ -911,7 +911,7 @@
1.22
1.23 consts
1.24 InverseZTransform :: "[bool, bool] => bool"
1.25 - ("((Script InverseZTransform (_ =))// (_))" 9)
1.26 + ("((Program InverseZTransform (_ =))// (_))" 9)
1.27
1.28 subsection \<open>Setup Parent Nodes in Hierarchy of Method\label{sec:cparentnode}\<close>
1.29
1.30 @@ -958,7 +958,7 @@
1.31 ("#Find", ["stepResponse n_eq"])],
1.32 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
1.33 errpats = [], nrls = e_rls},
1.34 - "Script InverseZTransform (Xeq::bool) =" ^ (*TODO boundVariable X_z*)
1.35 + "Program InverseZTransform (Xeq::bool) =" ^ (*TODO boundVariable X_z*)
1.36 " (let X = Take Xeq;" ^
1.37 " X = Rewrite ruleZY False X" ^
1.38 " in X)")]
1.39 @@ -987,7 +987,7 @@
1.40 subsection \<open>Stepwise Extend the Program\<close>
1.41 ML \<open>
1.42 val str =
1.43 - "Script InverseZTransform (Xeq::bool) = "^
1.44 + "Program InverseZTransform (Xeq::bool) = "^
1.45 " Xeq";
1.46 \<close>
1.47
1.48 @@ -996,7 +996,7 @@
1.49
1.50 ML \<open>
1.51 val str =
1.52 - "Script InverseZTransform (Xeq::bool) = "^
1.53 + "Program InverseZTransform (Xeq::bool) = "^
1.54 (*
1.55 * 1/z) instead of z ^^^ -1
1.56 *)
1.57 @@ -1013,7 +1013,7 @@
1.58 (*
1.59 * NONE
1.60 *)
1.61 - "Script InverseZTransform (Xeq::bool) = "^
1.62 + "Program InverseZTransform (Xeq::bool) = "^
1.63 (*
1.64 * (1/z) instead of z ^^^ -1
1.65 *)
1.66 @@ -1039,7 +1039,7 @@
1.67
1.68 ML \<open>
1.69 val str =
1.70 - "Script InverseZTransform (Xeq::bool) = "^
1.71 + "Program InverseZTransform (Xeq::bool) = "^
1.72 " (let X = Take Xeq; "^
1.73 " X' = Rewrite ruleZY False X; "^
1.74 " X' = (Rewrite_Set norm_Rational False) X'; "^
1.75 @@ -1054,9 +1054,9 @@
1.76 side. The equation itself consists of this denominator and tries to find
1.77 a $z$ for this the denominator is equal to zero.\<close>
1.78
1.79 -text \<open> dropped during switch from Script to partial_function:
1.80 +text \<open> dropped during switch from Program to partial_function:
1.81 val str =
1.82 - "Script InverseZTransform (X_eq::bool) = "^
1.83 + "Program InverseZTransform (X_eq::bool) = "^
1.84 " (let X = Take X_eq; "^
1.85 " X' = Rewrite ruleZY False X; "^
1.86 " X' = (Rewrite_Set norm_Rational False) X'; "^
1.87 @@ -1133,7 +1133,7 @@
1.88 ("#Find", ["stepResponse n_eq"])],
1.89 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls, prls = e_rls, crls = e_rls,
1.90 errpats = [], nrls = e_rls},
1.91 - "Script InverseZTransform (X_eq::bool) = "^
1.92 + "Program InverseZTransform (X_eq::bool) = "^
1.93 (*(1/z) instead of z ^^^ -1*)
1.94 "(let X = Take X_eq; "^
1.95 " X' = Rewrite ruleZY False X; "^
1.96 @@ -1308,7 +1308,7 @@
1.97 We see the SubProblem with correct arguments from searching next
1.98 step (program text !!!--->!!! STac (script tactic) with arguments
1.99 evaluated.)
1.100 - \item Do we have the right Script \ldots difference in the
1.101 + \item Do we have the right Program \ldots difference in the
1.102 arguments in the arguments\ldots
1.103 \begin{verbatim}
1.104 val Prog s =
1.105 @@ -1319,7 +1319,7 @@
1.106 \end{verbatim}
1.107 \ldots shows the right script. Difference in the arguments.
1.108 \item Test --- Why helpless here ? --- shows: \ttfamily replace
1.109 - no\_meth by [no\_meth] \normalfont in Script
1.110 + no\_meth by [no\_meth] \normalfont in Program
1.111 \end{itemize}
1.112 \<close>
1.113
1.114 @@ -1368,7 +1368,7 @@
1.115 \normalfont The only False is the reason: the Where (the precondition) is
1.116 False for good reasons: The precondition seems to check for linear
1.117 equations, not for the one we want to solve! Removed this error by
1.118 - correcting the Script from \ttfamily SubProblem (PolyEq',
1.119 + correcting the Program from \ttfamily SubProblem (PolyEq',
1.120 \lbrack linear,univariate,equation,
1.121 test\rbrack, \lbrack Test,solve\_linear\rbrack \normalfont to
1.122 \ttfamily SubProblem (PolyEq',\\ \lbrack abcFormula,degree\_2,
1.123 @@ -1382,7 +1382,7 @@
1.124 }
1.125 And the respective method in \ttfamily Knowledge/PolyEq.thy \normalfont
1.126 at the respective \ttfamily store\_pbt. \normalfont Or you leave the
1.127 - selection of the appropriate type to isac as done in the final Script ;-))
1.128 + selection of the appropriate type to isac as done in the final Program ;-))
1.129 \end{itemize}\<close>
1.130
1.131 ML \<open>