| Mon, 08 Mar 2021 09:11:09 +0100 |
\----- start update Isabelle2020 --> Isabelle2021
|
file | diff | annotate |
| Thu, 10 Dec 2020 14:38:32 +0100 |
step 3.4: stop SPARK as a model for investigating Isabelle's proof machinery
|
file | diff | annotate |
| Thu, 26 Nov 2020 12:24:37 +0100 |
initialise Calculation finished, check SPARK
|
file | diff | annotate |
| Wed, 25 Nov 2020 16:10:24 +0100 |
tuned
|
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 |
| Wed, 23 Sep 2020 15:18:07 +0200 |
\----- start update Isabelle2019 --> Isabelle2020
|
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 |
| Fri, 21 Mar 2014 10:45:03 +0100 |
tuned signature;
|
file | diff | annotate |
| Thu, 18 Apr 2013 17:07:01 +0200 |
simplifier uses proper Proof.context instead of historic type simpset;
|
file | diff | annotate |
| Mon, 19 Nov 2012 20:23:47 +0100 |
theorem status about oracles/futures is no longer printed by default;
|
file | diff | annotate |
| Mon, 23 Jul 2012 18:52:10 +0200 |
set_vcs now derives prefix from fully qualified procedure / function name
|
file | diff | annotate |
| Fri, 29 Jun 2012 09:45:48 +0200 |
Various improvements
|
file | diff | annotate |
| Fri, 11 May 2012 13:41:30 +0200 |
Fixed disambiguation of names (cf. 5759ecd5c905)
|
file | diff | annotate |
| Tue, 28 Feb 2012 11:10:09 +0100 |
Added infrastructure for mapping SPARK field / constructor names
|
file | diff | annotate |
| Mon, 27 Feb 2012 10:32:39 +0100 |
Use long prefix rather than short package name to disambiguate constant names
|
file | diff | annotate |
| Mon, 20 Feb 2012 16:09:58 +0100 |
Fixed bugs:
|
file | diff | annotate |
| Sat, 17 Dec 2011 12:10:37 +0100 |
tuned signature;
|
file | diff | annotate |
| Tue, 13 Dec 2011 23:23:51 +0100 |
'datatype' specifications allow explicit sort constraints;
|
file | diff | annotate |
| Fri, 02 Dec 2011 14:54:25 +0100 |
more antiquotations;
|
file | diff | annotate |
| Wed, 30 Nov 2011 23:30:08 +0100 |
discontinued obsolete datatype "alt_names";
|
file | diff | annotate |
| Sat, 19 Nov 2011 21:18:38 +0100 |
added ML antiquotation @{attributes};
|
file | diff | annotate |
| Sat, 19 Nov 2011 13:36:38 +0100 |
discontinued slightly odd write_prv, which would still write .prv files the first time, and deprive add-on tools from date stamp change (cf. 157e74588c49);
|
file | diff | annotate |
| Sun, 06 Nov 2011 16:41:53 +0100 |
write changed .prv files only, to avoid writing into src file-space by default;
|
file | diff | annotate |
| Fri, 02 Sep 2011 17:57:37 +0200 |
discontinued slightly odd "Defining record ..." message and corresponding quiet_mode;
|
file | diff | annotate |
| Thu, 04 Aug 2011 17:40:48 +0200 |
Pending FDL types may now be associated with Isabelle types as well.
|
file | diff | annotate |
| Fri, 08 Jul 2011 15:17:40 +0200 |
standardized String.concat towards implode;
|
file | diff | annotate |
| Thu, 09 Jun 2011 17:51:49 +0200 |
simplified Name.variant -- discontinued builtin fold_map;
|
file | diff | annotate |
| Wed, 27 Apr 2011 19:27:06 +0200 |
Properly treat proof functions with no arguments.
|
file | diff | annotate |
| Thu, 21 Apr 2011 12:56:27 +0200 |
discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
|
file | diff | annotate |
| Tue, 19 Apr 2011 14:17:41 +0200 |
- renamed enum type class to spark_enum, to avoid confusion with
|
file | diff | annotate |
| Mon, 18 Apr 2011 16:33:45 +0200 |
Package prefix is now taken into account when looking up user-defined
|
file | diff | annotate |
| Sat, 16 Apr 2011 16:15:37 +0200 |
modernized structure Proof_Context;
|
file | diff | annotate |
| Fri, 15 Apr 2011 15:33:57 +0200 |
Added command for associating user-defined types with SPARK types.
|
file | diff | annotate |
| Fri, 04 Mar 2011 17:39:30 +0100 |
spark_end now joins proofs of VCs before writing *.prv file.
|
file | diff | annotate |
| Thu, 03 Mar 2011 11:01:42 +0100 |
- Made sure that sort_defs is aware of constants introduced by add_type_def
|
file | diff | annotate |
| Wed, 26 Jan 2011 20:51:09 +0100 |
Replaced smod by standard mod operator to reflect actual behaviour
|
file | diff | annotate |
| Sat, 15 Jan 2011 12:35:29 +0100 |
Added new SPARK verification environment.
|
file | diff | annotate |