
diff -r b7071d1dd263 -r 007ef64dbb08 doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex
--- a/doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Mon Oct 31 18:28:36 2022 +0100
+++ b/doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Mon Nov 07 17:37:20 2022 +0100
@@ -802,12 +802,12 @@
    01  val inverse_z = Rls 
    02      {id       = "inverse_z",
    03       rew_ord  = dummy_ord,
-   04       erls     = Erls,
+   04       asm_rls     = Erls,
    05       rules    = [Thm ("rule1", @{thm rule1}), Thm ("rule2", @{thm rule1}), 
    06                   Thm ("rule3", @{thm rule3}), Thm ("rule4", @{thm rule4}), 
    07                   Thm ("rule5", @{thm rule5}), Thm ("rule6", @{thm rule6})],
    08       errpatts = [],
-   09       scr      = ""}
+   09       program      = ""}
 \end{verbatim}}
 
 \noindent The items, line by line, in the above record have the following purpose:
@@ -819,7 +819,7 @@
 line {\rm 12}).
 
 \item[03..04] both, (a) the rewrite-order~\cite{nipk:rew-all-that}
-\textit{rew\_ord} and (b) the rule-set \textit{erls} are trivial here:
+\textit{rew\_ord} and (b) the rule-set \textit{asm_rls} are trivial here:
 (a) the \textit{rules} in {\rm 07..12} don't need ordered rewriting
 and (b) the assumptions of the \textit{rules} need not be evaluated
 (they just go into the context during rewriting).
@@ -830,7 +830,7 @@
 and \textit{Calc} respectively; for the purpose of reflection both
 contain their identifiers.
 
-\item[08..09] are error-patterns not discussed here and \textit{scr}
+\item[08..09] are error-patterns not discussed here and \textit{program}
 is prepared to get a program, automatically generated by {\sisac} for
 producing intermediate rewrites when requested by the user.
 
@@ -1109,7 +1109,7 @@
    08          ("#Pre"  , ["(rhs X_eq) is_continuous_in D"]),
    09          ("#Find" , ["stepResponse n_eq"]),
    10          ("#Post" , [" TODO "])])
-   11        prls
+   11        where_rls
    12        NONE
    13        [["SignalProcessing","Z_Transform","Inverse"]]);
    14 *}
@@ -1163,9 +1163,9 @@
 %       because applied terms may be from 'subthy' as well as from super;
 %       thus we take 'maxthy'; see match_ags !*)
 %      cas   : term option,(*'CAS-command'*)
-%      prls  : rls,        (* for preds in where_*)
+%      where_rls  : rls,        (* for preds in where_*)
 %      where_: term list,  (* where - predicates*)
-%      ppc   : pat list,
+%      model   : pat list,
 %      (*this is the model-pattern; 
 %       it contains "#Given","#Where","#Find","#Relate"-patterns
 %       for constraints on identifiers see "fun copy_name"*)
@@ -1225,8 +1225,8 @@
    07        [ ("#Given", ["filterExpression X_eq", "domain D"]),
    08          ("#Pre"  , ["(rhs X_eq) is_continuous_in D"]),
    09          ("#Find" , ["stepResponse n_eq"]),
-   10        rew_ord  erls
-   11        srls  prls  nrls
+   10        rew_ord  asm_rls
+   11        prog_rls  where_rls  rew_rls
    12        errpats 
    13        program);
    14 *}
@@ -1244,8 +1244,8 @@
 is not started.
 
 \item[10..11] all concern rewriting (the respective data are defined elsewhere): \textit{rew\_ord} is the rewrite order~\cite{nipk:rew-all-that} in case
-\textit{program} contains a \textit{Rewrite} tactic; and in case the respective rule is a conditional rewrite-rule, \textit{erls} features evaluating the conditions. The rule-sets 
-\textit{srls, prls, nrls} feature evaluating (a) the ML-functions in the program (e.g.
+\textit{program} contains a \textit{Rewrite} tactic; and in case the respective rule is a conditional rewrite-rule, \textit{asm_rls} features evaluating the conditions. The rule-sets 
+\textit{prog_rls, where_rls, rew_rls} feature evaluating (a) the ML-functions in the program (e.g.
 \textit{lhs, argument\_in, rhs} in the program on p.\pageref{s:impl}, (b) the pre-condition analogous to the specification in line 11 on p.\pageref{exp-spec}
 and (c) is required for the derivation-machinery checking user-input formulas.
 
@@ -1466,7 +1466,7 @@
 \noindent The entry is perfect. So what is the reason~? Ah, probably there
 is something messed up with the many rule-sets in the method, see \S\ref{meth} ---
 right, the function \texttt{argument\_in} is not contained in the respective
-rule-set \textit{srls} \dots this just as an example of the intricacies in
+rule-set \textit{prog_rls} \dots this just as an example of the intricacies in
 debugging a program in the present state of the prototype.
 
 \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl}
@@ -2128,8 +2128,8 @@
 % LocalWords:  TP IST SPSC Telematics Dialogues dialogue HOL bool nat Hindley
 % LocalWords:  Milner tt Subproblem Formulae ruleset generalisation initialised
 % LocalWords:  axiomatization LCF Simplifiers simplifiers Isar rew Thm Calc SML
-% LocalWords:  recognised hoc Trueprop redexes Unsynchronized pre rhs ord erls
-% LocalWords:  srls prls nrls lhs errpats InverseZTransform SubProblem IDE IDEs
+% LocalWords:  recognised hoc Trueprop redexes Unsynchronized where_ rhs ord asm_rls
+% LocalWords:  prog_rls where_rls rew_rls lhs errpats InverseZTransform SubProblem IDE IDEs
 % LocalWords:  univariate jEdit rls RealDef calclist familiarisation ons pos eq
 % LocalWords:  mout ctree SignalProcessing frac ZZ Postcond Atools wiki SML's
 % LocalWords:  mechanisation multi




