| Fri, 27 Nov 2020 21:59:23 +0100 |
wenzelm |
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
|
file |
diff |
annotate
|
| Mon, 01 Oct 2018 12:41:35 +0200 |
wenzelm |
HOL-SPARK .prv files are no longer written to the file-system;
|
file |
diff |
annotate
|
| Thu, 31 May 2018 22:56:57 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sat, 14 May 2016 19:49:10 +0200 |
wenzelm |
toplevel theorem statements support 'if'/'for' eigen-context;
|
file |
diff |
annotate
|
| Sat, 14 May 2016 13:52:01 +0200 |
wenzelm |
reverted accidental commit;
|
file |
diff |
annotate
|
| Fri, 13 May 2016 20:24:10 +0200 |
wenzelm |
eliminated use of empty "assms";
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Sat, 04 Apr 2015 22:22:38 +0200 |
wenzelm |
more standard local_theory command setup;
|
file |
diff |
annotate
|
| Sat, 04 Apr 2015 14:04:11 +0200 |
wenzelm |
support private scope for individual local theory commands;
|
file |
diff |
annotate
|
| Mon, 03 Nov 2014 14:50:27 +0100 |
wenzelm |
eliminated unused int_only flag (see also c12484a27367);
|
file |
diff |
annotate
|
| Wed, 07 May 2014 12:59:15 +0200 |
wenzelm |
discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
|
file |
diff |
annotate
|
| 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
|