| Tue, 05 Jan 2021 17:29:39 +0100 |
step 4.7: cannot fill 2 gaps tracing Outer_Syntax .. Output.report
|
file | diff | annotate |
| Mon, 21 Dec 2020 15:13:49 +0100 |
step 4.6: two gaps in trace on SPARK
|
file | diff | annotate |
| Mon, 21 Dec 2020 11:55:10 +0100 |
step 4.5: separate trace for specific proof element
|
file | diff | annotate |
| Thu, 17 Dec 2020 18:00:27 +0100 |
step 4.4: call hierarchy up from Syntax.check_terms, partially
|
file | diff | annotate |
| Thu, 17 Dec 2020 09:10:30 +0100 |
step 4.2: writeln at calling Output.report uncover some of proof handling
|
file | diff | annotate |
| Tue, 17 Nov 2020 14:52:57 +0100 |
testbed for SPARK parsing g_c_d.siv
|
file | diff | annotate |
| Sun, 15 Nov 2020 15:26:52 +0100 |
insert @{print} to analyse HOL-SPARK parsing g_c_d.siv
|
file | diff | annotate |
| Mon, 02 Nov 2020 15:16:07 +0100 |
prepare Outer_Syntax.command..spark_open as model
|
file | diff | annotate |
| Mon, 26 Oct 2020 13:52:26 +0100 |
copy Outer_Syntax.command..spark_open as model for Isac Calculation
|
file | diff | annotate |
| Sat, 24 Oct 2020 12:31:22 +0200 |
exercise in manual type inference
|
file | diff | annotate |
| Thu, 22 Oct 2020 14:03:40 +0200 |
various trials to decompose Isabelle's proof machinery
|
file | diff | annotate |
| Tue, 03 Sep 2019 16:10:31 +0200 |
\----- start update Isabelle2018 --> Isabelle2019
|
file | diff | annotate |
| Wed, 22 Aug 2018 14:44:15 +0200 |
\----- start update Isabelle2017 --> Isabelle2018
|
file | diff | annotate |
| Fri, 19 Jan 2018 12:49:17 +0100 |
\----- start update Isabelle2015 --> Isabelle2017
|
file | diff | annotate |
| Sat, 05 Dec 2015 16:09:41 +0100 |
switched from Isabelle2014 to Isabelle2015, intermediate state
|
file | diff | annotate |
| Sat, 05 Jul 2014 11:01:53 +0200 |
prefer ac_simps collections over separate name bindings for add and mult
|
file | diff | annotate |
| Wed, 30 Apr 2014 15:43:44 +0200 |
Discontinued old spark_open; spark_open_siv is now spark_open
|
file | diff | annotate |
| Sat, 15 Jan 2011 12:35:29 +0100 |
Added new SPARK verification environment.
|
file | diff | annotate |