1.1 --- a/TODO.md Sun Dec 31 15:13:39 2023 +0100
1.2 +++ b/TODO.md Mon Jan 01 11:31:16 2024 +0100
1.3 @@ -43,6 +43,7 @@
1.4
1.5 * WN: cut out Calc.state_pre, Calc.state_post; only Ctree.state shall remain
1.6 ?or could that be reasonable also together with Isabelle/PIDE?
1.7 +* How can "./bin/isabelle build -v -b Specify_Phase" be done within Test_Isac?
1.8
1.9
1.10 ***** priority of WN items is top down, most urgent/simple on top
2.1 --- a/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy Sun Dec 31 15:13:39 2023 +0100
2.2 +++ b/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy Mon Jan 01 11:31:16 2024 +0100
2.3 @@ -22,10 +22,10 @@
2.4 \chapter{Interactive Specification in an \isac-Calculation}
2.5 %#############################################################################
2.6 This is a copy of the submission to the post-proceedings of ThEdu'23
2.7 -under the title \textit{``Interactive Formal Specification for Mathematical Problems of Engineers''} \footnote{
2.8 +under the title \textit{``Interactive Formal Specification for Mathematical Problems of Engineers''}~\footnote{
2.9 \url{https://static.miraheze.org/isacwiki/a/a0/Wneuper-3-adopt-post.pdf)}}.
2.10 Thus this chapter is preliminary, it will be supplemented and probably split
2.11 -up in the following.
2.12 +up in the following development process.
2.13
2.14 \section{Introduction} \label{sect:introduction}
2.15 %==============================================================================
2.16 @@ -268,8 +268,8 @@
2.17 operational power in different number ranges (e.g. in the complex numbers
2.18 each polynomial has roots, in the real numbers it may have none).
2.19 Thus it \textbf{restricts Isabelle's contexts to
2.20 -particular theories}, for instance to \texttt{Int.thy}, to \texttt{Real.thy} or
2.21 -to \texttt{Complex.thy}.
2.22 +particular theories}, for instance to @{theory HOL.Int}, to @{theory HOL.Real} or
2.23 +to @{theory HOL.Complex}.
2.24
2.25 \item\label{UR:model} \textbf{No need for formal logic}:
2.26 The formal specification of a problem must be
2.27 @@ -311,7 +311,7 @@
2.28 \end{itemize}
2.29
2.30 \item\label{UR:toggle-problem-method} Within the @{theory_text Specification} the
2.31 -\textbf{\emph{Model} serves two purposes}: for the \emph{Problem\_Ref} it shows
2.32 +\textbf{@{theory_text Model} serves two purposes}: for the \emph{Problem\_Ref} it shows
2.33 the fields from \emph{Given} to \emph{Relate} according to Pt.\ref{UR:model}
2.34 and for \emph{Method\_Ref} it shows the guard of the program guiding
2.35 the \emph{Solution}; for details see \cite{wn:lucin-thedu20}. A
2.36 @@ -468,21 +468,21 @@
2.37
2.38 \begin{small}
2.39 \begin{verbatim}
2.40 - 01 val demo_example = ("The efficiency of an electrical coil depends on the mass of the kernel. Given is a kernel with cross-sectional area determined by two rectangles of same shape as shown in the figure. Given a radius r = 7, determine the length u and width v of the rectangles such that the cross-sectional area A (and thus the mass of the kernel) is a maximum. + Figure",
2.41 - 02 ([
2.42 - 03 (*Problem model:*)
2.43 - 04 "Constants [r = (7::real)]", "Maximum A", "AdditionalValues [u, v]",
2.44 - 05 "Extremum (A = 2 * u * v - u \<up> 2)",
2.45 - 06 "SideConditions [((u::real) / 2) \<up> 2 + (v / 2) \<up> 2 = r \<up> 2]",
2.46 - 07 "SideConditions [(u::real) / 2 = r * sin \<alpha>, v / 2 = r * cos \<alpha>]",
2.47 - 08 (*MethodC model:*)
2.48 - 09 "FunctionVariable u", "FunctionVariable v",
2.49 - 10 "FunctionVariable \<alpha>",
2.50 - 11 "Domain {0 <..< r}",
2.51 - 12 "Domain {0 <..< \<pi> / 2}",
2.52 - 13 "ErrorBound (\<epsilon> = (0::real))"]: TermC.as_string list,
2.53 - 14 ("Diff_App", ["univariate_calculus", "Optimisation"],
2.54 - 15 ["Optimisation", "by_univariate_calculus"]): References.T)): Formalise.T
2.55 + 01 val demo_example = ("The efficiency of an electrical coil depends on ..",
2.56 + 02 ([
2.57 + 03 (*Problem model:*)
2.58 + 04 "Constants [r = (7::real)]", "Maximum A", "AdditionalValues [u, v]",
2.59 + 05 "Extremum (A = 2 * u * v - u \<up> 2)",
2.60 + 06 "SideConditions [((u::real) / 2) \<up> 2 + (v / 2) \<up> 2 = r \<up> 2]",
2.61 + 07 "SideConditions [(u::real) / 2 = r * sin \<alpha>, v / 2 = r * cos \<alpha>]",
2.62 + 08 (*MethodC model:*)
2.63 + 09 "FunctionVariable u", "FunctionVariable v",
2.64 + 10 "FunctionVariable \<alpha>",
2.65 + 11 "Domain {0 <..< r}",
2.66 + 12 "Domain {0 <..< \<pi> / 2}",
2.67 + 13 "ErrorBound (\<epsilon> = (0::real))"]: TermC.as_string list,
2.68 + 14 ("Diff_App", ["univariate_calculus", "Optimisation"],
2.69 + 15 ["Optimisation", "by_univariate_calculus"]): References.T)): Formalise.T
2.70 \end{verbatim}\label{src:demo-expl}
2.71 \end{small}
2.72 The text in line \texttt{01} exceeds the line limit, it has already been