Walther Neuper <walther.neuper@jku.at> [Fri, 22 Jan 2021 11:27:47 +0100] rev 60147
step 5.2: shift tests from Test_Parse_Isac.thy to test/../parseC.sml
Walther Neuper <walther.neuper@jku.at> [Sun, 17 Jan 2021 15:25:27 +0100] rev 60146
step 5.1: separate code for keyword Example to preliminary file
Walther Neuper <walther.neuper@jku.at> [Sun, 17 Jan 2021 13:16:25 +0100] rev 60145
step 5: cleanup previous steps; status quo
Walther Neuper <walther.neuper@jku.at> [Thu, 14 Jan 2021 16:14:27 +0100] rev 60144
step 4.8: close all gaps in trace of SPARK gcd
notes on trace at click on <have "0 < x mod d">:
* writeln NOT contributing to trace are outcommented
* writeln contributing to trace are marked (*have*)
Walther Neuper <walther.neuper@jku.at> [Mon, 11 Jan 2021 13:01:08 +0100] rev 60143
try to close 2 gaps in trace
note: the gaps are marked ??? 1 ??? and ??? 2 ???
Walther Neuper <walther.neuper@jku.at> [Wed, 06 Jan 2021 11:17:28 +0100] rev 60142
tuned
Walther Neuper <walther.neuper@jku.at> [Tue, 05 Jan 2021 17:29:39 +0100] rev 60141
step 4.7: cannot fill 2 gaps tracing Outer_Syntax .. Output.report
note: see Greatest_Common_Divisor.thy, subsection ?fill gaps in traces?
Walther Neuper <walther.neuper@jku.at> [Mon, 21 Dec 2020 15:13:49 +0100] rev 60140
step 4.6: two gaps in trace on SPARK
note: no caller found for "Syntax.read_props" and "Proof.have"
Walther Neuper <walther.neuper@jku.at> [Mon, 21 Dec 2020 11:55:10 +0100] rev 60139
step 4.5: separate trace for specific proof element
the proof element is "from ?0 < d?" plus "have "0 ? c mod d""
Walther Neuper <walther.neuper@jku.at> [Thu, 17 Dec 2020 18:00:27 +0100] rev 60138
step 4.4: call hierarchy up from Syntax.check_terms, partially