| Wed, 30 Apr 2014 15:43:44 +0200 |
berghofe |
Discontinued old spark_open; spark_open_siv is now spark_open
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:35:39 +0200 |
wenzelm |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 17:39:03 +0100 |
wenzelm |
clarifed module name;
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 17:39:20 +0100 |
wenzelm |
modernized theory setup;
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 17:29:58 +0100 |
wenzelm |
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 15:29:25 +0200 |
wenzelm |
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
|
file |
diff |
annotate
|
| Tue, 08 Jan 2013 22:10:02 +0100 |
wenzelm |
disable interactive mode of Specification.theorem with its slow printing of results;
|
file |
diff |
annotate
|
| Wed, 19 Sep 2012 14:47:15 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Thu, 23 Aug 2012 15:43:28 +0200 |
wenzelm |
added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
|
file |
diff |
annotate
|
| Fri, 29 Jun 2012 09:45:48 +0200 |
berghofe |
Various improvements
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 21:06:31 +0100 |
wenzelm |
optional 'includes' element for long theorem statements;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Tue, 28 Feb 2012 11:10:09 +0100 |
berghofe |
Added infrastructure for mapping SPARK field / constructor names
|
file |
diff |
annotate
|
| Fri, 08 Jul 2011 14:37:19 +0200 |
wenzelm |
more abstract Thy_Load.load_file/use_file for external theory resources;
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 17:17:49 +0200 |
wenzelm |
clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
|
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
|
| Sun, 20 Mar 2011 17:40:45 +0100 |
wenzelm |
replaced File.check by specific File.check_file, File.check_dir;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 16:38:54 +0100 |
wenzelm |
more basic use of Path.position/File.read;
|
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 18:42:12 +0100 |
wenzelm |
simplified Thy_Info.check_file -- discontinued load path;
|
file |
diff |
annotate
|
| Sun, 16 Jan 2011 17:21:13 +0100 |
berghofe |
Tuned show_status
|
file |
diff |
annotate
|
| Sun, 16 Jan 2011 15:04:16 +0100 |
wenzelm |
more standard command descriptions;
|
file |
diff |
annotate
|
| Sat, 15 Jan 2011 12:35:29 +0100 |
berghofe |
Added new SPARK verification environment.
|
file |
diff |
annotate
|