| Mon, 19 Nov 2012 20:23:47 +0100 |
wenzelm |
theorem status about oracles/futures is no longer printed by default;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2012 18:52:10 +0200 |
berghofe |
set_vcs now derives prefix from fully qualified procedure / function name
|
file |
diff |
annotate
|
| Fri, 29 Jun 2012 09:45:48 +0200 |
berghofe |
Various improvements
|
file |
diff |
annotate
|
| Fri, 11 May 2012 13:41:30 +0200 |
berghofe |
Fixed disambiguation of names (cf. 5759ecd5c905)
|
file |
diff |
annotate
|
| Tue, 28 Feb 2012 11:10:09 +0100 |
berghofe |
Added infrastructure for mapping SPARK field / constructor names
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 10:32:39 +0100 |
berghofe |
Use long prefix rather than short package name to disambiguate constant names
|
file |
diff |
annotate
|
| Mon, 20 Feb 2012 16:09:58 +0100 |
berghofe |
Fixed bugs:
|
file |
diff |
annotate
|
| Sat, 17 Dec 2011 12:10:37 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 23:23:51 +0100 |
wenzelm |
'datatype' specifications allow explicit sort constraints;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 14:54:25 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 23:30:08 +0100 |
wenzelm |
discontinued obsolete datatype "alt_names";
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 21:18:38 +0100 |
wenzelm |
added ML antiquotation @{attributes};
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 13:36:38 +0100 |
wenzelm |
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 |
wenzelm |
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 |
wenzelm |
discontinued slightly odd "Defining record ..." message and corresponding quiet_mode;
|
file |
diff |
annotate
|
| Thu, 04 Aug 2011 17:40:48 +0200 |
berghofe |
Pending FDL types may now be associated with Isabelle types as well.
|
file |
diff |
annotate
|
| Fri, 08 Jul 2011 15:17:40 +0200 |
wenzelm |
standardized String.concat towards implode;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 17:51:49 +0200 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 19:27:06 +0200 |
berghofe |
Properly treat proof functions with no arguments.
|
file |
diff |
annotate
|
| Thu, 21 Apr 2011 12:56:27 +0200 |
wenzelm |
discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 14:17:41 +0200 |
berghofe |
- renamed enum type class to spark_enum, to avoid confusion with
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 16:33:45 +0200 |
berghofe |
Package prefix is now taken into account when looking up user-defined
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 15 Apr 2011 15:33:57 +0200 |
berghofe |
Added command for associating user-defined types with SPARK types.
|
file |
diff |
annotate
|
| Fri, 04 Mar 2011 17:39:30 +0100 |
berghofe |
spark_end now joins proofs of VCs before writing *.prv file.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2011 11:01:42 +0100 |
berghofe |
- 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 |
berghofe |
Replaced smod by standard mod operator to reflect actual behaviour
|
file |
diff |
annotate
|
| Sat, 15 Jan 2011 12:35:29 +0100 |
berghofe |
Added new SPARK verification environment.
|
file |
diff |
annotate
|