equal
deleted
inserted
replaced
67 \<close> |
67 \<close> |
68 |
68 |
69 section \<open>Stepwise Development\<close> |
69 section \<open>Stepwise Development\<close> |
70 |
70 |
71 subsection \<open>Specification Phase\<close> |
71 subsection \<open>Specification Phase\<close> |
72 text \<open> UPDATE: |
72 text \<open> |
73 1. The \<open>Example\<close> below is a minimal adaptation of \<open>problem pbl_bieg : "Biegelinien" ..\<close> |
73 stepwise development to be inspected from |
74 in Knowledge/Biegelinie.thy. |
74 https://hg.risc.uni-linz.ac.at/wneuper/isa/rev/9d98791b4080 |
75 2. GOON |
75 onwards. |
76 \<close> |
76 \<close> |
77 |
77 |
78 (* |
|
79 vvvvvvv why raises \<open>Example\<close> exception Option raised (line 82 of "General/basics.ML")? Although |
|
80 * code (Outer_Syntax.command..Example..) and |
|
81 * application (Example pbl_bieg : "Biegelinien".) are exact copies from Makarius? |
|
82 * Although the application below with \<open>problem\<close> works? |
|
83 * Although \<open>ExampleSPARK\<close> is disambiguated in Calculation_OLD.thy ?!? |
|
84 HOW CAN SUCH AN ERROR BE INVESTIGATED ? debugger ? .. ? |
|
85 Example problem*) |
|
86 Example pbl_bieg : "Biegelinien" = |
78 Example pbl_bieg : "Biegelinien" = |
87 Method: "IntegrierenUndKonstanteBestimmen2" |
79 Method: "IntegrierenUndKonstanteBestimmen2" |
88 Given: "Traegerlaenge l_l" "Streckenlast q_q" |
80 Given: "Traegerlaenge l_l" "Streckenlast q_q" |
89 (* Where: "0 < l_l" ...wait for < and handling Arbfix*) |
81 (* Where: "0 < l_l" ...wait for < and handling Arbfix*) |
90 Find: "Biegelinie b_b" |
82 Find: "Biegelinie b_b" |