neuper@42314
|
1 |
(* Title: todo's for isac core
|
neuper@42314
|
2 |
Author: Walther Neuper 111013
|
neuper@42314
|
3 |
(c) copyright due to lincense terms.
|
neuper@42314
|
4 |
*)
|
wneuper@59504
|
5 |
theory TODO
|
wneuper@59504
|
6 |
imports "~~/src/Doc/Prog_Prove/LaTeXsugar"
|
wneuper@59504
|
7 |
begin
|
neuper@42314
|
8 |
|
wneuper@59574
|
9 |
section \<open>TODOs from current changesets\<close>
|
wneuper@59568
|
10 |
text\<open>
|
wneuper@59568
|
11 |
Shift more complicated issues from the next subsection to the next but one!
|
wneuper@59568
|
12 |
\<close>
|
wneuper@59574
|
13 |
subsection \<open>Current changeset\<close>
|
wneuper@59574
|
14 |
text \<open>
|
wneuper@59569
|
15 |
\begin{itemize}
|
wneuper@59601
|
16 |
\item xxx
|
walther@59763
|
17 |
\item ??????????? WHY CAN LucinNEW.by_tactic NOT BE REPLACED BY Step_Solve.by_tactic ???????????
|
walther@59659
|
18 |
\item xxx
|
walther@59767
|
19 |
\item ? datatype Tactic.input: MathEngBasic/tactic-def.sml + tactic.sml ?!?
|
walther@59635
|
20 |
\item xxx
|
walther@59635
|
21 |
\item rm test/..--- check Scripts ---
|
walther@59635
|
22 |
\item xxx
|
walther@59718
|
23 |
\item reformat + rename "fun eval_leaf"+"fun get_stac"
|
walther@59635
|
24 |
(*1*)(*2*)
|
walther@59635
|
25 |
?consistency with subst term?
|
walther@59730
|
26 |
\item Tactic.Rewrite*': drop "bool"
|
walther@59635
|
27 |
\item xxx
|
walther@59635
|
28 |
\item exception PROG analogous to TERM
|
walther@59635
|
29 |
\item xxx
|
walther@59635
|
30 |
\item xxx
|
walther@59635
|
31 |
\item xxx
|
walther@59635
|
32 |
\item Prog_Tac: fun get_stac takes both Prog_Tac + Program --- wait for separate Taciical
|
walther@59635
|
33 |
then shift into common descendant
|
walther@59635
|
34 |
rename get_stac --> ?ptac?
|
wneuper@59601
|
35 |
\item xxx
|
wneuper@59601
|
36 |
\item xxx
|
wneuper@59601
|
37 |
\item xxx
|
wneuper@59586
|
38 |
\item separate code required in both, ProgLang & Interpret
|
wneuper@59591
|
39 |
\item xxx
|
wneuper@59591
|
40 |
\item /-------------------------------------------------------------------
|
wneuper@59591
|
41 |
\item check occurences of KEStore_Elems.add_rlss [("list_rls",
|
wneuper@59591
|
42 |
\item rename list_rls accordingly
|
wneuper@59591
|
43 |
\item ------------------------------------------------------------------/
|
wneuper@59591
|
44 |
\item xxx
|
wneuper@59591
|
45 |
\item xxx
|
wneuper@59591
|
46 |
\item rm Float
|
wneuper@59591
|
47 |
\item xxx
|
wneuper@59586
|
48 |
\item signature LIBRARY_C
|
wneuper@59586
|
49 |
\item Program.thy (*=========== record these ^^^ in 'tacs' in program.ML =========*)
|
wneuper@59586
|
50 |
\item sig/struc ..elems --> elem
|
wneuper@59586
|
51 |
\item xxx
|
wneuper@59586
|
52 |
\item xxx
|
wneuper@59586
|
53 |
\end{itemize}
|
wneuper@59574
|
54 |
\item xxx
|
wneuper@59582
|
55 |
\item xxx
|
walther@59633
|
56 |
\item distribute test/../scrtools.sml
|
wneuper@59574
|
57 |
\item xxx
|
wneuper@59574
|
58 |
\item xxx
|
walther@59691
|
59 |
\item simplify calls of scan_dn1, scan_dn2 etc
|
wneuper@59586
|
60 |
\item open Istate in LucinNEW
|
wneuper@59574
|
61 |
\end{itemize}
|
wneuper@59574
|
62 |
\<close>
|
wneuper@59574
|
63 |
subsection \<open>Postponed from current changeset\<close>
|
wneuper@59574
|
64 |
text \<open>
|
wneuper@59574
|
65 |
\begin{itemize}
|
walther@59648
|
66 |
\item xxx
|
walther@59734
|
67 |
\item re-organise code for Interpret
|
walther@59734
|
68 |
\begin{itemize}
|
walther@59743
|
69 |
\item Step*:
|
walther@59734
|
70 |
\begin{itemize}
|
walther@59743
|
71 |
\item Step_Specify in Specify/step-specify.sml in analogy to Interpret/... TODO
|
walther@59742
|
72 |
\begin{itemize}
|
walther@59743
|
73 |
\item Step_Specify.check <-- Applicable.applicable_in
|
walther@59743
|
74 |
\item Step_Specify.add <-- Generate.generate1
|
walther@59762
|
75 |
\item Step_Specify.by_formula: ?term? -> Ctree.state -> ...stay as is
|
walther@59742
|
76 |
\end{itemize}
|
walther@59743
|
77 |
\item Step_Solve in Interpret/step-solve.sml
|
walther@59734
|
78 |
\begin{itemize}
|
walther@59743
|
79 |
\item Step_Solve.check <-- Applicable.applicable_in
|
walther@59746
|
80 |
inserts all data into Tactic.T available -- not all are at time of call!
|
walther@59743
|
81 |
\item Step_Solve.add <-- Generate.generate1
|
walther@59762
|
82 |
\item Step_Solve.by_formula : term -> Ctree.state -> ...stay as is
|
walther@59734
|
83 |
\end{itemize}
|
walther@59743
|
84 |
\item Step in MathEngine/step.sml
|
walther@59743
|
85 |
\begin{itemize}
|
walther@59743
|
86 |
\item Step.check : Step_Specify.check | Step_Solve.check depending on pos'
|
walther@59746
|
87 |
inserts all data into Tactic.T available -- not all are at time of call!
|
walther@59743
|
88 |
\item Step.add : Step_Specify.add | Step_Solve.add depending on pos'
|
walther@59743
|
89 |
\item Step.by_tactic : Step_Specify.by_tactic | Step_Solve.by_tactic depending on pos'
|
walther@59743
|
90 |
\item Step.by_formula: Step_Specify.by_formula | Step_Solve.by_formula depending on pos'
|
walther@59760
|
91 |
\item Step.do_next : Step_Specify.find_next | Step_Solve.find_next depending on pos'
|
walther@59743
|
92 |
\end{itemize}
|
walther@59761
|
93 |
\item NOTE on mut.rec: Step.do_next calls Step_Solve.do_next + Step_Specify.do_next
|
walther@59761
|
94 |
^ Math_Engine.nxt_specify_
|
walther@59762
|
95 |
so some restructuring is required.
|
walther@59761
|
96 |
INTERMEDIATE STEP: Step.do_next is still Math_Engine.do_next
|
walther@59743
|
97 |
\end{itemize}
|
walther@59734
|
98 |
\item xxx
|
walther@59734
|
99 |
\item xxx
|
walther@59734
|
100 |
\end{itemize}
|
walther@59734
|
101 |
\item xxx
|
walther@59733
|
102 |
\item xxx
|
walther@59760
|
103 |
\item decompose do_next, by_tactic: mutual recursion only avoids multiple generate1
|
walther@59743
|
104 |
! ^^^ in find_next_tactic --- ? ? ? in locate_input_tactic ?
|
walther@59731
|
105 |
\item xxx
|
walther@59731
|
106 |
\item Generate.generate1 thy is redundant: is the same during pbl, thus lookup spec
|
walther@59731
|
107 |
\item xxx
|
walther@59731
|
108 |
\item NEW structure Step.applicable Step.add
|
walther@59731
|
109 |
^applicable_in ^generate1
|
walther@59731
|
110 |
\item xxx
|
walther@59729
|
111 |
\item revise Pstate {or, ...}; strange occurrence in program without Tactical.Or documented here
|
walther@59648
|
112 |
\item xxx
|
walther@59659
|
113 |
\item shift tests into NEW model.sml (upd, upds_envv, ..)
|
walther@59659
|
114 |
\item xxx
|
walther@59731
|
115 |
\item NEW structures
|
walther@59731
|
116 |
\begin{itemize}
|
walther@59762
|
117 |
\item MathEngBasic/calculation.sml ??("Calc" is occupied ?!?) ? rename Calc --> Calc_
|
walther@59731
|
118 |
\begin{itemize}
|
walther@59762
|
119 |
\item rename existing Calc --> Calc_
|
walther@59762
|
120 |
\item ? type Calc.T = CTree.state ?
|
walther@59731
|
121 |
\item xxx
|
walther@59762
|
122 |
\item xxx
|
walther@59731
|
123 |
\item xxx
|
walther@59731
|
124 |
\end{itemize}
|
walther@59731
|
125 |
\end{itemize}
|
walther@59648
|
126 |
\item xxx
|
wneuper@59583
|
127 |
\item clarify handling of contexts
|
wneuper@59583
|
128 |
\begin{itemize}
|
walther@59748
|
129 |
\item xxx
|
walther@59748
|
130 |
\item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt
|
walther@59748
|
131 |
\item xxx
|
wneuper@59583
|
132 |
\item Check_Elementwise "Assumptions": prerequisite for ^^goal
|
wneuper@59586
|
133 |
rm tactic Check_elementwise "Assumptions" in a way, which keeps it for Minisubpbl
|
wneuper@59601
|
134 |
rm Assumptions :: bool (* TODO: remove with making ^^^ idle *)
|
wneuper@59583
|
135 |
\item xxx
|
walther@59633
|
136 |
\item cleanup fun me:
|
wneuper@59592
|
137 |
fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
|
wneuper@59592
|
138 |
| me*) (_, tac) p _(*NEW remove*) pt =
|
wneuper@59592
|
139 |
+ -------------------------^^^^^^
|
wneuper@59592
|
140 |
\item xxx
|
walther@59748
|
141 |
\item remove ctxt from Tactic.T; this makes use of ctxt more explicit (e.g. in Lucin)
|
walther@59748
|
142 |
\begin{itemize}
|
walther@59748
|
143 |
\item Tactic.Apply_Method' (mI, _, _, _(*ctxt ?!?*))) .. remove ctxt
|
walther@59748
|
144 |
\item rm ctxt from Subproblem' (is separated in associate!))
|
walther@59748
|
145 |
\end{itemize}
|
wneuper@59583
|
146 |
\item check Tactic.Subproblem': are 2 terms required?
|
wneuper@59583
|
147 |
\item xxx
|
wneuper@59583
|
148 |
\item Test_Some.--- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts --
|
wneuper@59583
|
149 |
--: wait for deleting Check_Elementwise Assumptions
|
wneuper@59583
|
150 |
\item xxx
|
walther@59691
|
151 |
\item lucas-intrpreter.scan_dn1: Generate.generate1 (Celem.assoc_thy "Isac_Knowledge")
|
wneuper@59583
|
152 |
\end{itemize}
|
wneuper@59583
|
153 |
\item xxx
|
walther@59635
|
154 |
\item xxx
|
wneuper@59583
|
155 |
\item complete mstools.sml (* survey on handling contexts:
|
wneuper@59583
|
156 |
\item xxx
|
wneuper@59578
|
157 |
\item xxx
|
wneuper@59579
|
158 |
\item istate
|
wneuper@59579
|
159 |
\begin{itemize}
|
wneuper@59586
|
160 |
\item datatype L,R,D --> Istate
|
wneuper@59586
|
161 |
\item xxx
|
wneuper@59586
|
162 |
\item xxx
|
wneuper@59586
|
163 |
\item xxx
|
walther@59691
|
164 |
\item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr .use Term.exists_Const
|
wneuper@59586
|
165 |
\item xxx
|
walther@59748
|
166 |
\item scrstate2str --> pstate2str
|
wneuper@59586
|
167 |
\item xxx
|
wneuper@59586
|
168 |
\item after review of Rrls, detail ?-->? istate
|
wneuper@59579
|
169 |
\item locate_input_tactic: get_simplifier cstate (*TODO: shift to init_istate*)
|
wneuper@59579
|
170 |
\item xxx
|
wneuper@59586
|
171 |
\item push srls into pstate
|
walther@59690
|
172 |
\item lucas-intrpreter.locate_input_tactic: scan_to_tactic1 srls tac cstate (progr, Rule.e_rls)
|
wneuper@59586
|
173 |
^^^^^^^^^^
|
wneuper@59579
|
174 |
\item xxx
|
wneuper@59579
|
175 |
\item xxx
|
wneuper@59579
|
176 |
\end{itemize}
|
wneuper@59579
|
177 |
\item xxx
|
wneuper@59579
|
178 |
\item trace_script: replace ' by " in writeln
|
wneuper@59578
|
179 |
\item xxx
|
wneuper@59578
|
180 |
\item librarys.ml --> libraryC.sml + text from termC.sml
|
wneuper@59578
|
181 |
\item xxx
|
wneuper@59586
|
182 |
\item xxx
|
wneuper@59577
|
183 |
\item xxx
|
wneuper@59574
|
184 |
\item xxx
|
wneuper@59574
|
185 |
\item xxx
|
wneuper@59579
|
186 |
\item xxx
|
walther@59731
|
187 |
\item concentrate "insert_assumptions" for locate_input_tactic in "associate", ?OR? Tactic.insert_assumptions
|
walther@59743
|
188 |
DONE for find_next_tactic by Tactic.insert_assumptions m' ctxt
|
wneuper@59577
|
189 |
\begin{itemize}
|
wneuper@59577
|
190 |
\item rm from "generate1" ("Detail_Set_Inst'", Tactic.Detail_Set' ?)
|
wneuper@59577
|
191 |
\item shift from "applicable_in..Apply_Method" to ? ? ? (is ONLY use-case in appl.sml))
|
wneuper@59583
|
192 |
\item ?"insert_assumptions" necessary in "init_pstate" ?+++? in "applicable_in" ?+++? "associate"
|
wneuper@59577
|
193 |
\item xxx
|
wneuper@59577
|
194 |
\item xxx
|
walther@59743
|
195 |
\item DO DELETIONS AFTER analogous concentrations in find_next_tactic
|
wneuper@59577
|
196 |
\end{itemize}
|
wneuper@59577
|
197 |
\item xxx
|
wneuper@59579
|
198 |
\item ? what is the difference headline <--> cascmd in
|
wneuper@59579
|
199 |
Subproblem' (spec, oris, headline, fmz_, context, cascmd)
|
wneuper@59569
|
200 |
\item xxx
|
wneuper@59592
|
201 |
\item inform: TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr --> parseNEW context istr
|
wneuper@59574
|
202 |
\item extract common code from associate.. stac2tac_
|
wneuper@59574
|
203 |
\end{itemize}
|
wneuper@59574
|
204 |
\<close>
|
wneuper@59574
|
205 |
|
wneuper@59574
|
206 |
section \<open>Separated tasks\<close>
|
wneuper@59574
|
207 |
text \<open>
|
wneuper@59574
|
208 |
\<close>
|
wneuper@59574
|
209 |
subsection \<open>Simple\<close>
|
wneuper@59574
|
210 |
text \<open>
|
walther@59604
|
211 |
\item xxx
|
walther@59603
|
212 |
\item xxx
|
walther@59603
|
213 |
\item check location of files:
|
walther@59603
|
214 |
test/Tools/isac/Interpret/ptyps.thy
|
walther@59603
|
215 |
test/Tools/isac/Specify.ptyps.sml
|
walther@59603
|
216 |
\item xxx
|
walther@59603
|
217 |
\item check occurences of Atools in src/ test/
|
walther@59603
|
218 |
\item xxx
|
walther@59603
|
219 |
\item drop drop_questionmarks_
|
walther@59603
|
220 |
\item xxx
|
walther@59603
|
221 |
\item Const ("Atools.pow", _) ---> Const ("Base_Tool.pow", _)
|
walther@59603
|
222 |
\item rename Base_Tool.thy <--- Base_Tool
|
walther@59603
|
223 |
\item xxx
|
walther@59603
|
224 |
\item test/.. tools.sml, atools.sml, scrtools.sml ...
|
walther@59603
|
225 |
\item xxx
|
wneuper@59574
|
226 |
\item Diff.thy: differentiateX --> differentiate after removal of script-constant
|
wneuper@59574
|
227 |
\item Test.thy: met_test_sqrt2: deleted?!
|
wneuper@59574
|
228 |
\item xxx
|
wneuper@59577
|
229 |
\item Applicable.applicable_in --> Applicable.tactic_at
|
wneuper@59574
|
230 |
\item xxx
|
wneuper@59578
|
231 |
\item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
|
wneuper@59578
|
232 |
\item xxx
|
wneuper@59582
|
233 |
\item TermC.vars_of replace by vars (recognises numerals)
|
wneuper@59578
|
234 |
\item xxx
|
wneuper@59574
|
235 |
\item xxx
|
wneuper@59574
|
236 |
\end{itemize}
|
wneuper@59574
|
237 |
\<close>
|
wneuper@59574
|
238 |
subsection \<open>Simple but laborous\<close>
|
wneuper@59574
|
239 |
text \<open>
|
wneuper@59574
|
240 |
\begin{itemize}
|
wneuper@59579
|
241 |
\item prep_met
|
wneuper@59579
|
242 |
\begin{itemize}
|
wneuper@59579
|
243 |
\item rename field scr in meth
|
wneuper@59579
|
244 |
\item xxx
|
wneuper@59591
|
245 |
\item Rule.rew_ord' := overwritel (! Rule.rew_ord', (*<<<---- use KEStore.xxx, too*)
|
wneuper@59591
|
246 |
\item xxx
|
wneuper@59579
|
247 |
\item check match between args of partial_function and model-pattern of meth;
|
wneuper@59579
|
248 |
provide error message.
|
wneuper@59579
|
249 |
\item xxx
|
wneuper@59579
|
250 |
\item automatically extrac rls from program-code
|
wneuper@59579
|
251 |
? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?
|
wneuper@59579
|
252 |
\item xxx
|
wneuper@59579
|
253 |
\item xxx
|
wneuper@59579
|
254 |
\item xxx
|
wneuper@59579
|
255 |
\end{itemize}
|
wneuper@59574
|
256 |
\item xxx
|
wneuper@59579
|
257 |
\item drop "init_form" and use "Take" in programs (start with latter!)
|
wneuper@59574
|
258 |
\item xxx
|
wneuper@59582
|
259 |
\item deprive Check_elementwise, but keep it for Minisubpl
|
wneuper@59582
|
260 |
(which checks for Check_Postcond separated by another tactic)
|
wneuper@59582
|
261 |
This seems a prerequisite for appropriate handling of contexts at Check_Postcond.
|
wneuper@59582
|
262 |
\item xxx
|
wneuper@59574
|
263 |
\end{itemize}
|
wneuper@59574
|
264 |
\<close>
|
wneuper@59574
|
265 |
subsection \<open>Questionable\<close>
|
wneuper@59574
|
266 |
text \<open>
|
wneuper@59574
|
267 |
\begin{itemize}
|
wneuper@59574
|
268 |
\item finish output of trace_script with Check_Postcond (useful for SubProblem)
|
wneuper@59574
|
269 |
\item unify in signature LANGUAGE_TOOLS =\\
|
wneuper@59574
|
270 |
val pblterm: Rule.domID -> Celem.pblID -> term vvv vvv\\
|
wneuper@59574
|
271 |
val subpbl: string -> string list -> term unify with ^^^
|
wneuper@59574
|
272 |
\item xxx
|
walther@59675
|
273 |
\item Telem.safe is questionable: has it been replaced by Safe_Step, Not_Derivable, Helpless, etc?
|
walther@59676
|
274 |
Note: replacement of Istate.safe by Istate.appy_ didn't care much about Telem.safe.
|
walther@59675
|
275 |
If Telem.safe is kept, consider merge with CTbasic.ostate
|
wneuper@59574
|
276 |
\item xxx
|
walther@59743
|
277 |
\item remove find_next_tactic from solve Apply_Method';
|
walther@59696
|
278 |
this enforces Pos.at_first_tactic, which should be dropped, too.
|
walther@59696
|
279 |
\item xxx
|
wneuper@59574
|
280 |
\item xxx
|
wneuper@59574
|
281 |
\end{itemize}
|
wneuper@59574
|
282 |
\<close>
|
wneuper@59574
|
283 |
section \<open>Complex, related to --> other tasks\<close>
|
wneuper@59574
|
284 |
text \<open>
|
wneuper@59574
|
285 |
\<close>
|
walther@59615
|
286 |
subsection \<open>Exception Size raised\<close>
|
walther@59615
|
287 |
text \<open>
|
walther@59615
|
288 |
During update Isabelle2018 --> Isabelle2019 we noticed, that
|
walther@59615
|
289 |
"isabelle build" uses resources more efficiently than "isabelle jedit".
|
walther@59615
|
290 |
The former works, but the latter causes
|
walther@59615
|
291 |
\begin{itemize}
|
walther@59615
|
292 |
\item "Exception- Size raised"
|
walther@59615
|
293 |
in Build_Thydata.thy
|
walther@59615
|
294 |
\item "exception Size raised (line 169 of "./basis/LibrarySupport.sml")"
|
walther@59615
|
295 |
in test/../biegelinie-*.xml.
|
walther@59615
|
296 |
\end{itemize}
|
walther@59615
|
297 |
This has been detected after changeset (30cd47104ad7) "lucin: reorganise theories in ProgLang".
|
walther@59615
|
298 |
|
walther@59615
|
299 |
Find tools to investigate the Exception, and find ways around it eventually.
|
walther@59615
|
300 |
\<close>
|
walther@59636
|
301 |
subsection \<open>Cleanup & review signatures wrt. implementation.pdf canonical argument order\<close>
|
wneuper@59574
|
302 |
text \<open>
|
walther@59636
|
303 |
\begin{itemize}
|
walther@59636
|
304 |
\item there are comments in several signatures
|
walther@59636
|
305 |
\item ML_file "~~/src/Tools/isac/Interpret/specification-elems.sml" can be (almost) deleted
|
walther@59636
|
306 |
\item src/../Frontend/: signatures missing
|
walther@59636
|
307 |
\item xxx
|
walther@59636
|
308 |
\end{itemize}
|
wneuper@59574
|
309 |
\<close>
|
wneuper@59593
|
310 |
subsection \<open>overall structure of code\<close>
|
wneuper@59593
|
311 |
text \<open>
|
wneuper@59593
|
312 |
\begin{itemize}
|
wneuper@59593
|
313 |
\item try to separate Isac_Knowledge from MathEngine
|
wneuper@59593
|
314 |
common base: Knowledge_Author / ..??
|
wneuper@59593
|
315 |
\item xxx
|
wneuper@59594
|
316 |
\item ML_file "~~/src/Tools/isac/Interpret/ctree.sml" (*shift to base in common with Interpret*)
|
wneuper@59594
|
317 |
\item xxx
|
wneuper@59593
|
318 |
\item xxx
|
wneuper@59593
|
319 |
\item xxx
|
wneuper@59593
|
320 |
\end{itemize}
|
wneuper@59593
|
321 |
\<close>
|
walther@59760
|
322 |
subsection \<open>solve, loc_solve_, by_tactic, do_next, ...\<close>
|
wneuper@59574
|
323 |
text \<open>
|
walther@59733
|
324 |
unify to calcstate, calcstate', ?Ctree.state?
|
wneuper@59574
|
325 |
\begin{itemize}
|
walther@59751
|
326 |
\item by_tactic Check_Postcond' needs NO 2.find_next_tactic
|
walther@59733
|
327 |
solve Check_Postcond' needs, because NO prog_result in Tactic.input
|
walther@59733
|
328 |
and applicable_in cannot get it.
|
wneuper@59583
|
329 |
\item xxx
|
wneuper@59574
|
330 |
\item adopt the same for specification phase
|
wneuper@59574
|
331 |
\item xxx
|
wneuper@59574
|
332 |
\end{itemize}
|
wneuper@59574
|
333 |
\<close>
|
wneuper@59574
|
334 |
subsection \<open>Review modelling- + specification-phase\<close>
|
wneuper@59574
|
335 |
text \<open>
|
wneuper@59574
|
336 |
\begin{itemize}
|
wneuper@59574
|
337 |
\item "--- hack for funpack: generalise handling of meths which extend problem items ---"
|
wneuper@59569
|
338 |
\begin{itemize}
|
wneuper@59574
|
339 |
\item see several locations of hack in code
|
wneuper@59574
|
340 |
\item these locations are NOT sufficient, see
|
wneuper@59574
|
341 |
test/../biegelinie-3.sml --- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---
|
wneuper@59574
|
342 |
\item "fun associate" "match_ags ..dI" instead "..pI" breaks many tests, however,
|
wneuper@59574
|
343 |
this would be according to survey Notes (3) in src/../calchead.sml.
|
wneuper@59574
|
344 |
\end{itemize}
|
wneuper@59574
|
345 |
\item see "failed trial to generalise handling of meths"98298342fb6d
|
wneuper@59574
|
346 |
\item abstract specify + nxt_specif to common aux-funs;
|
wneuper@59574
|
347 |
see e.g. "--- hack for funpack: generalise handling of meths which extend problem items ---"
|
wneuper@59574
|
348 |
\item xxx
|
wneuper@59574
|
349 |
\item type model = itm list ?
|
wneuper@59574
|
350 |
\item review survey Notes in src/../calchead.sml: they are questionable
|
wneuper@59574
|
351 |
\item review copy-named, probably two issues commingled
|
wneuper@59574
|
352 |
\begin{itemize}
|
wneuper@59574
|
353 |
\item special handling of "#Find#, because it is not a formal argument of partial_function
|
wneuper@59574
|
354 |
\item special naming for solutions of equation solving: x_1, x_2, ...
|
wneuper@59569
|
355 |
\end{itemize}
|
wneuper@59569
|
356 |
\item xxx
|
walther@59634
|
357 |
\item structure Tactic Specify -?-> Proglang (would require Model., Selem.)
|
walther@59634
|
358 |
\item xxx
|
wneuper@59574
|
359 |
\item this has been written in one go:
|
wneuper@59574
|
360 |
\begin{itemize}
|
wneuper@59574
|
361 |
\item reconsidering Model.max_vt, use problem with meth ["DiffApp","max_by_calculus"]
|
wneuper@59574
|
362 |
\item reconsider add_field': where is it used for what? Shift into mk_oris
|
wneuper@59574
|
363 |
\item reconsider match_itms_oris: where is it used for what? max_vt ONLY???
|
wneuper@59574
|
364 |
\item in Specify_Method search root-oris for items (e.g. "errorBound"), #1# in survey
|
wneuper@59574
|
365 |
\item Specify_Problem, Specify_Method: check respective identifiers after re-Specify_
|
wneuper@59574
|
366 |
(relevant for pre-condition)
|
wneuper@59574
|
367 |
\item unify match_ags to mk_oris1..N with different args (fmz | pat list, pbl | meth
|
wneuper@59574
|
368 |
\item
|
wneuper@59574
|
369 |
\end{itemize}
|
wneuper@59574
|
370 |
\end{itemize}
|
wneuper@59574
|
371 |
\<close>
|
wneuper@59574
|
372 |
subsection \<open>taci list, type step\<close>
|
wneuper@59574
|
373 |
text \<open>
|
walther@59762
|
374 |
taci was, most likely, invented to make "fun me" more efficient by avoiding duplicate rewrite,
|
walther@59762
|
375 |
and probably, because the Kernel interface separated setNextTactic and applyTactic.
|
walther@59762
|
376 |
Both are no good reasons to make code more complicated. For instance Math_Engine.do_next
|
walther@59762
|
377 |
could drop half of the code. So try to use Ctree.state only.
|
wneuper@59574
|
378 |
\begin{itemize}
|
walther@59762
|
379 |
\item xxx
|
walther@59762
|
380 |
\item Step* functions should return Ctree.state instead of Chead.calcstate'
|
walther@59762
|
381 |
\item xxx
|
wneuper@59574
|
382 |
\item states.sml: check, when "length tacis > 1"
|
wneuper@59574
|
383 |
\item in Test_Isac.thy there is only 1 error in Interpret/inform.sml
|
wneuper@59574
|
384 |
\item (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
|
wneuper@59569
|
385 |
\item xxx
|
walther@59762
|
386 |
\item brute force setting all empty ([], [], ptp) but ptp causes errors -- investigate!
|
walther@59762
|
387 |
\item xxx
|
wneuper@59573
|
388 |
\end{itemize}
|
wneuper@59574
|
389 |
\<close>
|
wneuper@59574
|
390 |
subsection \<open>Ctree\<close>
|
wneuper@59574
|
391 |
text \<open>
|
wneuper@59568
|
392 |
\begin{itemize}
|
wneuper@59574
|
393 |
\item review get_ctxt, update_ctxt, get_istate, upd_istate, upd_ctxt,
|
wneuper@59574
|
394 |
<---> update_loc', repl_loc (remove the latter)
|
wneuper@59568
|
395 |
\item delete field ctxt in PblObj in favour of loc
|
wneuper@59568
|
396 |
\item xxx
|
wneuper@59574
|
397 |
\item xxx
|
wneuper@59568
|
398 |
\end{itemize}
|
wneuper@59574
|
399 |
\<close>
|
wneuper@59574
|
400 |
subsection \<open>replace theory/thy by context/ctxt\<close>
|
wneuper@59574
|
401 |
text \<open>
|
wneuper@59574
|
402 |
\begin{itemize}
|
walther@59660
|
403 |
\item xxx
|
walther@59748
|
404 |
\item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt
|
walther@59748
|
405 |
special case: Tactic.Refine_Problem
|
walther@59748
|
406 |
\item xxx
|
walther@59748
|
407 |
\item theory can be retrieved from ctxt by Proof_Context.theory_of
|
walther@59660
|
408 |
\item xxx
|
wneuper@59577
|
409 |
\item cleaup the many conversions string -- theory
|
wneuper@59577
|
410 |
\item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ?
|
wneuper@59574
|
411 |
\item 1. Rewrite.eval_true_, then
|
walther@59718
|
412 |
Lucin.interpret_leaf, Rewrite.eval_prog_expr, Generate.generate1, Lucin.stac2tac.
|
wneuper@59577
|
413 |
\item fun associate
|
wneuper@59592
|
414 |
let val thy = Celem.assoc_thy "Isac_Knowledge";(*TODO*)
|
wneuper@59574
|
415 |
\item xxx
|
wneuper@59574
|
416 |
\item xxx
|
wneuper@59577
|
417 |
\item xxx
|
wneuper@59574
|
418 |
\end{itemize}
|
wneuper@59574
|
419 |
\<close>
|
wneuper@59583
|
420 |
subsection \<open>Rfuns, Begin_/End_Detail', Rrls, Istate\<close>
|
wneuper@59574
|
421 |
text \<open>
|
wneuper@59562
|
422 |
\begin{itemize}
|
wneuper@59573
|
423 |
\item removing from_pblobj_or_detail' causes many strange errors
|
wneuper@59573
|
424 |
\item ^^^+ see from_pblobj_or_detail_thm, from_pblobj_or_detail_calc, ...
|
wneuper@59573
|
425 |
\item xxx
|
wneuper@59569
|
426 |
\item probably only "normal_form" seems to be needed
|
wneuper@59569
|
427 |
\item deleted Rfuns in NEW "locate_input_tactic": no active test for "locate_rule"
|
wneuper@59569
|
428 |
but that seems desirable
|
wneuper@59569
|
429 |
\item ?how is the relation to reverse-rewriting ???
|
wneuper@59569
|
430 |
\item "Rfuns" markers in test/../rational
|
wneuper@59562
|
431 |
\item xxx
|
walther@59667
|
432 |
\item datatype istate (Istate.T): remove RrlsState, pstate: use Rrls only for creating results beyond
|
wneuper@59573
|
433 |
rewriting and/or respective intermediate steps (e.g. cancellation of fractions).
|
wneuper@59583
|
434 |
Thus we get a 1-step-action which does NOT require a state beyond istate/pstate.
|
wneuper@59573
|
435 |
Thus we drastically reduce complexity, also get rid of "fun from_pblobj_or_detail_calc" , etc.
|
wneuper@59573
|
436 |
\item debug ^^^ related: is there an occurence of Steps with more than 1 element?
|
wneuper@59569
|
437 |
\item xxx
|
walther@59760
|
438 |
\item and do_next (* WN1907: ?only for Begin_/End_Detail' DEL!!!*)
|
wneuper@59573
|
439 |
\item xxx
|
wneuper@59573
|
440 |
\item shouldn't go Rfuns from Rewrite --> Rewrite_Set; they behave similar to "fun interSteps" ?
|
wneuper@59562
|
441 |
\end{itemize}
|
wneuper@59574
|
442 |
\<close>
|
wneuper@59574
|
443 |
subsection \<open>Inverse_Z_Transform.thy\<close>
|
wneuper@59574
|
444 |
text \<open>
|
wneuper@59538
|
445 |
\begin{itemize}
|
wneuper@59550
|
446 |
\item\label{new-var-rhs} rule1..6, ruleZY introduce new variables on the rhs of the rewrite-rule.
|
wneuper@59550
|
447 |
? replace rewriting with substitution ?!?
|
wneuper@59537
|
448 |
The problem is related to the decision of typing for "d_d" and making bound variables free (while
|
wneuper@59550
|
449 |
shifting specific handling in equation solving etc. to the meta-logic).
|
wneuper@59550
|
450 |
\item Find "stepResponse (x[n::real]::bool)" is superfluous, because immediately used by
|
wneuper@59550
|
451 |
rewrite-rules; see \ref{new-var-rhs}.
|
wneuper@59538
|
452 |
\item Reconsider whole problem:
|
wneuper@59538
|
453 |
input only the polynomial as argument of partial_function, in ([1], Frm) compile lhs "X z" ?
|
wneuper@59538
|
454 |
\end{itemize}
|
wneuper@59574
|
455 |
\<close>
|
wneuper@59574
|
456 |
subsection \<open>Adopt Isabelle's numerals for Isac\<close>
|
wneuper@59574
|
457 |
text \<open>
|
wneuper@59540
|
458 |
\begin{itemize}
|
wneuper@59574
|
459 |
\item replace numerals of type "real" by "nat" in some specific functions from ListC.thy
|
wneuper@59574
|
460 |
and have both representations in parallel for "nat".
|
wneuper@59574
|
461 |
\item xxx
|
wneuper@59574
|
462 |
\item xxx
|
wneuper@59540
|
463 |
\end{itemize}
|
wneuper@59574
|
464 |
\<close>
|
walther@59636
|
465 |
subsection \<open>Auto_Prog\<close>
|
wneuper@59588
|
466 |
text \<open>
|
walther@59636
|
467 |
two issues:
|
walther@59636
|
468 |
(1) fun prep_rls creates a Program with too general and wrong types.
|
walther@59636
|
469 |
(2) generated Programs (huge since strings are coded in ASCII) stored in rls drives
|
walther@59636
|
470 |
Build_Thydata towards limits of resources.
|
walther@59636
|
471 |
\begin{itemize}
|
walther@59636
|
472 |
\item rename Auto_Prog.prep_rls --> Auto_Prog.generate
|
walther@59636
|
473 |
\item Auto_Prog.generate : term -> rls -> (*Program*)term
|
walther@59636
|
474 |
Ctree.current_formula---^^^^
|
walther@59636
|
475 |
\item xxx
|
walther@59636
|
476 |
\item xxx
|
walther@59636
|
477 |
\item generate Program on demand in from_pblobj_or_detail'
|
walther@59636
|
478 |
\item xxx
|
walther@59636
|
479 |
\item xxx
|
walther@59636
|
480 |
\end{itemize}
|
walther@59636
|
481 |
\<close>
|
walther@59636
|
482 |
subsection \<open>Redesign specify-phase\<close>
|
walther@59636
|
483 |
text \<open>
|
walther@59636
|
484 |
\begin{itemize}
|
walther@59636
|
485 |
\item xxx
|
walther@59636
|
486 |
\item Separate Specify/ Interpret/ MathEngine/
|
walther@59636
|
487 |
MathEngine.solve, ...,
|
walther@59636
|
488 |
? or identify "layers" like in Isabelle?
|
walther@59636
|
489 |
\item xxx
|
walther@59636
|
490 |
\item xxx
|
walther@59636
|
491 |
\end{itemize}
|
wneuper@59588
|
492 |
\<close>
|
wneuper@59591
|
493 |
subsection \<open>Redesign thms for equation solver\<close>
|
wneuper@59591
|
494 |
text \<open>
|
wneuper@59591
|
495 |
Existing solver is structured along the WRONG assumption,
|
wneuper@59591
|
496 |
that Poly.thy must be the LAST thy among all thys involved.
|
wneuper@59591
|
497 |
|
wneuper@59591
|
498 |
Preliminary solution: all inappropriately located thms are collected in Base_Tools.thy
|
wneuper@59591
|
499 |
\<close>
|
wneuper@59574
|
500 |
subsection \<open>Finetunig required for xmldata\<close>
|
wneuper@59574
|
501 |
text \<open>
|
wneuper@59574
|
502 |
See xmldata https://intra.ist.tugraz.at/hg/isac/rev/5b222a649390
|
wneuper@59574
|
503 |
and in kbase html-representation generated from these xmldata.
|
wneuper@59574
|
504 |
Notes in ~~/xmldata/TODO.txt.
|
wneuper@59574
|
505 |
\<close>
|
wneuper@59574
|
506 |
|
wneuper@59574
|
507 |
section \<open>Hints for further development\<close>
|
wneuper@59574
|
508 |
text \<open>
|
wneuper@59574
|
509 |
\<close>
|
wneuper@59591
|
510 |
subsection \<open>Coding standards & some explanations for math-authors\<close>
|
wneuper@59591
|
511 |
text \<open>copy from doc/math-eng.tex WN.28.3.03
|
wneuper@59591
|
512 |
WN071228 extended\<close>
|
wneuper@59591
|
513 |
|
wneuper@59591
|
514 |
subsubsection \<open>Identifiers\<close>
|
wneuper@59591
|
515 |
text \<open>Naming is particularily crucial, because Isabelles name space is global, and isac does
|
wneuper@59591
|
516 |
not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds
|
wneuper@59591
|
517 |
reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the
|
wneuper@59591
|
518 |
problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc.
|
wneuper@59591
|
519 |
However, all the cases (1)..(4) require different typing for one and the same
|
wneuper@59591
|
520 |
identifier {\tt probe} which is impossible, and actually leads to strange errors
|
wneuper@59591
|
521 |
(for instance (1) is used as string, except in a script addressing a Subproblem).
|
wneuper@59591
|
522 |
|
wneuper@59591
|
523 |
These are the preliminary rules for naming identifiers>
|
wneuper@59591
|
524 |
\begin{description}
|
wneuper@59591
|
525 |
\item [elements of a key] into the hierarchy of problems or methods must not contain
|
wneuper@59591
|
526 |
capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}.
|
wneuper@59591
|
527 |
\item [descriptions in problem-patterns] must contain at least 1 capital letter and
|
wneuper@59591
|
528 |
must not contain underscores, e.g. {\tt Probe, forPolynomials}.
|
wneuper@59591
|
529 |
\item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus
|
wneuper@59591
|
530 |
beware of conflicts~!
|
wneuper@59591
|
531 |
\item [script identifiers] always end with {\tt Program}, e.g. {\tt ProbeScript}.
|
wneuper@59591
|
532 |
\item [???] ???
|
wneuper@59591
|
533 |
\item [???] ???
|
wneuper@59591
|
534 |
\end{description}
|
wneuper@59591
|
535 |
%WN071228 extended\<close>
|
wneuper@59591
|
536 |
|
wneuper@59591
|
537 |
subsubsection \<open>Rule sets\<close>
|
wneuper@59591
|
538 |
text \<open>The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML
|
wneuper@59591
|
539 |
where it can be viewed using the knowledge browsers.
|
wneuper@59591
|
540 |
|
wneuper@59591
|
541 |
There are rulesets visible to the student, and there are rulesets visible (in general) only for
|
wneuper@59591
|
542 |
math authors. There are also rulesets which {\em must} exist for {\em each} theory;
|
wneuper@59591
|
543 |
these contain the identifier of the respective theory (including all capital letters)
|
wneuper@59591
|
544 |
as indicated by {\it Thy} below.
|
wneuper@59591
|
545 |
|
wneuper@59591
|
546 |
\begin{description}
|
wneuper@59591
|
547 |
\item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a
|
wneuper@59591
|
548 |
normalform for all terms which can be expressed by the definitions of the respective theory
|
wneuper@59591
|
549 |
(and the respective parents).
|
wneuper@59591
|
550 |
\item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms
|
wneuper@59591
|
551 |
which can be expressed by the definitions of the respective theory (and the respective parents)
|
wneuper@59591
|
552 |
such, that the rewrites can be presented to the student.
|
wneuper@59591
|
553 |
\item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with
|
wneuper@59591
|
554 |
numerical constants only (i.e. all terms which can be expressed by the definitions of
|
wneuper@59591
|
555 |
the respective theory and the respective parent theories). In particular, this ruleset includes
|
wneuper@59591
|
556 |
evaluating in/equalities with numerical constants only.
|
wneuper@59591
|
557 |
WN.3.7.03: may be dropped due to more generality: numericals and non-numericals
|
wneuper@59591
|
558 |
are logically equivalent, where the latter often add to the assumptions
|
wneuper@59591
|
559 |
(e.g. in Check_elementwise).
|
wneuper@59591
|
560 |
\end{description}
|
wneuper@59591
|
561 |
|
wneuper@59591
|
562 |
The above rulesets are all visible to the user, and also may be input;
|
wneuper@59591
|
563 |
thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,
|
wneuper@59591
|
564 |
KEStore_Elems.get_rlss). All these rulesets must undergo a preparation
|
wneuper@59591
|
565 |
using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.
|
wneuper@59591
|
566 |
The following rulesets are used for internal purposes and usually invisible to the (naive) user:
|
wneuper@59591
|
567 |
|
wneuper@59591
|
568 |
\begin{description}
|
wneuper@59591
|
569 |
\item [*\_erls] TODO
|
wneuper@59591
|
570 |
\item [*\_prls]
|
wneuper@59591
|
571 |
\item [*\_srls]
|
wneuper@59591
|
572 |
\end{description}
|
wneuper@59591
|
573 |
{\tt Rule.append_rls, Rule.merge_rls, remove_rls} TODO
|
wneuper@59591
|
574 |
\<close>
|
wneuper@59591
|
575 |
|
wneuper@59574
|
576 |
subsection \<open>get proof-state\<close>
|
wneuper@59574
|
577 |
text \<open>
|
wneuper@59574
|
578 |
Re: [isabelle] Programatically get "this"
|
wneuper@59574
|
579 |
----------------------------------------------------
|
wneuper@59574
|
580 |
So here is my (Makarius') version of your initial example, following these principles:
|
wneuper@59574
|
581 |
begin{verbatim}
|
wneuper@59574
|
582 |
notepad
|
wneuper@59574
|
583 |
begin
|
wneuper@59574
|
584 |
assume a: A
|
wneuper@59574
|
585 |
ML_val \<open>
|
wneuper@59574
|
586 |
val ctxt = @{context};
|
wneuper@59558
|
587 |
|
wneuper@59574
|
588 |
val this_name =
|
walther@59748
|
589 |
Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN);
|
wneuper@59574
|
590 |
val this = #thms (the (Proof_Context.lookup_fact ctxt this_name));
|
wneuper@59574
|
591 |
\<close>
|
wneuper@59574
|
592 |
end
|
wneuper@59574
|
593 |
end{verbatim}
|
wneuper@59574
|
594 |
\<close>
|
wneuper@59574
|
595 |
subsection \<open>write Specification to jEdit\<close>
|
wneuper@59574
|
596 |
text \<open>
|
wneuper@59574
|
597 |
Re: [isabelle] Printing terms with type annotations
|
wneuper@59574
|
598 |
----------------------------------------------------
|
wneuper@59574
|
599 |
On 06/02/2019 17:52, Moa Johansson wrote:
|
wneuper@59574
|
600 |
>
|
wneuper@59574
|
601 |
> I’m writing some code that should create a snippet of Isar script.
|
wneuper@59574
|
602 |
|
wneuper@59574
|
603 |
This is how Sledgehammer approximates this:
|
wneuper@59574
|
604 |
|
wneuper@59574
|
605 |
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML#l299
|
wneuper@59574
|
606 |
|
wneuper@59574
|
607 |
(The module name already shows that the proper terminology is "Isar
|
wneuper@59574
|
608 |
proof" (or "Isar proof text"). Proof scripts are a thing from the past,
|
wneuper@59574
|
609 |
before Isar. You can emulate old-style proof scripts via a sequence of
|
wneuper@59574
|
610 |
'apply' commands, but this is improper Isar.)
|
wneuper@59574
|
611 |
|
wneuper@59574
|
612 |
Note that there is no standard function in Isabelle/Pure, because the
|
wneuper@59574
|
613 |
problem to print just the right amount of type information is very
|
wneuper@59574
|
614 |
complex and not fully solved. One day, after 1 or 2 rounds of
|
wneuper@59574
|
615 |
refinements over the above approach, it might become generally available.
|
wneuper@59574
|
616 |
\<close>
|
wneuper@59574
|
617 |
subsection \<open>follow Isabelle conventions (*Does not yet work in Isabelle2018\<close>
|
wneuper@59574
|
618 |
text \<open>
|
wneuper@59574
|
619 |
isabelle update -u path_cartouches
|
wneuper@59574
|
620 |
isabelle update -u inner_syntax_cartouches
|
wneuper@59574
|
621 |
\<close>
|
wneuper@59582
|
622 |
section \<open>Questions to Isabelle experts\<close>
|
wneuper@59582
|
623 |
text \<open>
|
wneuper@59582
|
624 |
\begin{itemize}
|
wneuper@59591
|
625 |
\item what is the actual replacement of "hg log --follow" ?
|
wneuper@59591
|
626 |
\item xxx
|
wneuper@59582
|
627 |
\item how HANDLE these exceptions, e.g.:
|
wneuper@59582
|
628 |
Syntax.read_term ctxt "Randbedingungen y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]"
|
wneuper@59582
|
629 |
GIVES
|
wneuper@59582
|
630 |
"Inner syntax error
|
wneuper@59582
|
631 |
Failed to parse term"
|
wneuper@59582
|
632 |
\item xxx
|
walther@59734
|
633 |
\item how cope with "exception Size raised (line 171 of "./basis/LibrarySupport.sml")"
|
walther@59734
|
634 |
e.g. in test/Interpret/lucas-interpreter.sml
|
wneuper@59582
|
635 |
\item xxx
|
wneuper@59582
|
636 |
\item xxx
|
wneuper@59582
|
637 |
\end{itemize}
|
wneuper@59582
|
638 |
\<close>
|
wneuper@59582
|
639 |
|
wneuper@59574
|
640 |
section \<open>For copy & paste\<close>
|
wneuper@59574
|
641 |
text \<open>
|
wneuper@59582
|
642 |
\begin{itemize}
|
wneuper@59558
|
643 |
\begin{itemize}
|
wneuper@59558
|
644 |
\item xxx
|
wneuper@59540
|
645 |
\begin{itemize}
|
wneuper@59558
|
646 |
\item xxx
|
wneuper@59540
|
647 |
\begin{itemize}
|
wneuper@59558
|
648 |
\item xxx
|
wneuper@59574
|
649 |
\begin{itemize}
|
wneuper@59574
|
650 |
\item xxx
|
wneuper@59574
|
651 |
\end{itemize}
|
wneuper@59540
|
652 |
\end{itemize}
|
wneuper@59540
|
653 |
\end{itemize}
|
wneuper@59504
|
654 |
\end{itemize}
|
wneuper@59504
|
655 |
\end{itemize}
|
wneuper@59504
|
656 |
\<close>
|
wneuper@59574
|
657 |
subsection \<open>xxx\<close>
|
wneuper@59574
|
658 |
subsubsection \<open>xxx\<close>
|
neuper@52150
|
659 |
end
|