equal
deleted
inserted
replaced
46 \<open>Problem_Ref: "univariate_calculus/Optimisation"\<close> are redundant; the latter is for input, |
46 \<open>Problem_Ref: "univariate_calculus/Optimisation"\<close> are redundant; the latter is for input, |
47 the former is given initially and needs to be updated in accordance to \<open>Problem_Ref\<close>. |
47 the former is given initially and needs to be updated in accordance to \<open>Problem_Ref\<close>. |
48 \<close> |
48 \<close> |
49 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*) |
49 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*) |
50 |
50 |
51 Example "Diff_App/No.123 a" |
51 Example "Diff_App-No.123a" |
52 Specification: |
52 Specification: |
53 Model: |
53 Model: |
54 Given: \<open>Constants r = 7\<close> |
54 Given: \<open>Constants r = 7\<close> |
55 Where: \<open>0 < r\<close> |
55 Where: \<open>0 < r\<close> |
56 Find: \<open>Maximum A\<close> \<open>AdditionalValues u, v\<close> |
56 Find: \<open>Maximum A\<close> \<open>AdditionalValues u, v\<close> |
67 text \<open> |
67 text \<open> |
68 This is presented to the student in one go in order to start interactive Specification. |
68 This is presented to the student in one go in order to start interactive Specification. |
69 \<close> |
69 \<close> |
70 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*) |
70 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*) |
71 |
71 |
72 Example "Diff_App/No.123 a" |
72 Example "Diff_App-No.123a" |
73 Specification: |
73 Specification: |
74 Model: |
74 Model: |
75 Given: \<open>Constants _\<close> |
75 Given: \<open>Constants _\<close> |
76 Where: \<open>0 < r\<close> |
76 Where: \<open>0 < r\<close> |
77 Find: \<open>Maximum _\<close> \<open>AdditionalValues _\<close> |
77 Find: \<open>Maximum _\<close> \<open>AdditionalValues _\<close> |
84 (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close> |
84 (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close> |
85 |
85 |
86 subsubsection \<open>Plain Example\<close> |
86 subsubsection \<open>Plain Example\<close> |
87 text \<open> |
87 text \<open> |
88 This can occur in between text offering to start an interactive Calculation by using |
88 This can occur in between text offering to start an interactive Calculation by using |
89 "Diff_App/No.123 a" as a link. |
89 "Diff_App-No.123a" as a link. |
90 \<close> |
90 \<close> |
91 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*) |
91 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*) |
92 |
92 |
93 Example "Diff_App/No.123 a" |
93 Example "Diff_App-No.123a" |
94 |
94 |
95 (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close> |
95 (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close> |
96 |
96 |
97 subsubsection \<open>Immediate Start of Interactive Solving\<close> |
97 subsubsection \<open>Immediate Start of Interactive Solving\<close> |
98 text \<open> |
98 text \<open> |
100 where Specification usually is not interesting to students |
100 where Specification usually is not interesting to students |
101 and thus done automatically by ISAC in the background. |
101 and thus done automatically by ISAC in the background. |
102 \<close> |
102 \<close> |
103 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*) |
103 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*) |
104 |
104 |
105 Example "Diff_App/No.123 a" |
105 Example "Diff_App-No.123a" |
106 Problem "univariate_calculus/Optimisation" |
106 Problem "univariate_calculus/Optimisation" |
107 Specification: |
107 Specification: |
108 Solution: |
108 Solution: |
109 |
109 |
110 (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close> |
110 (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close> |
117 (TODO: method/program for \<open>Problem "univariate_calculus/Optimisation"\<close>) |
117 (TODO: method/program for \<open>Problem "univariate_calculus/Optimisation"\<close>) |
118 The Model of a method is usually called a guard. |
118 The Model of a method is usually called a guard. |
119 \<close> |
119 \<close> |
120 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*) |
120 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*) |
121 |
121 |
122 Example "Diff_App/No.123 a" |
122 Example "Diff_App-No.123a" |
123 Problem "univariate_calculus/Optimisation" |
123 Problem "univariate_calculus/Optimisation" |
124 Specification: |
124 Specification: |
125 Model: |
125 Model: |
126 Given: \<open>Constants r = 7\<close> |
126 Given: \<open>Constants r = 7\<close> |
127 Where: \<open>0 < r\<close> |
127 Where: \<open>0 < r\<close> |
191 Stepwise development of \<open>Outer_Syntax.command \<^command_keyword>\<open>Example\<close>\<close> begins with |
191 Stepwise development of \<open>Outer_Syntax.command \<^command_keyword>\<open>Example\<close>\<close> begins with |
192 the changeset https://hg.risc.uni-linz.ac.at/wneuper/isa/rev/9d98791b4080 |
192 the changeset https://hg.risc.uni-linz.ac.at/wneuper/isa/rev/9d98791b4080 |
193 in the repository. |
193 in the repository. |
194 |
194 |
195 The intermediate steps below will be deleted as soon as all above representations |
195 The intermediate steps below will be deleted as soon as all above representations |
196 of Example "Diff_App/No.123 a" work out. |
196 of Example "Diff_App-No.123a" work out. |
197 \<close> |
197 \<close> |
198 |
198 |
199 subsubsection \<open>Complete Specification at once\<close> |
199 subsubsection \<open>Complete Specification at once\<close> |
200 Example "Diff_App-No.123a" |
200 Example "Diff_App-No.123a" |
201 Specification: |
201 Specification: |