src/HOL/SPARK/Tools/spark_commands.ML
Sat, 14 May 2016 13:52:01 +0200 wenzelm reverted accidental commit;
Fri, 13 May 2016 20:24:10 +0200 wenzelm eliminated use of empty "assms";
Wed, 13 Apr 2016 18:01:05 +0200 wenzelm eliminated "xname" and variants;
Fri, 25 Sep 2015 20:37:59 +0200 wenzelm moved remaining display.ML to more_thm.ML;
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
Sat, 04 Apr 2015 22:22:38 +0200 wenzelm more standard local_theory command setup;
Sat, 04 Apr 2015 14:04:11 +0200 wenzelm support private scope for individual local theory commands;
Mon, 03 Nov 2014 14:50:27 +0100 wenzelm eliminated unused int_only flag (see also c12484a27367);
Wed, 07 May 2014 12:59:15 +0200 wenzelm discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
Wed, 30 Apr 2014 15:43:44 +0200 berghofe Discontinued old spark_open; spark_open_siv is now spark_open
Mon, 31 Mar 2014 12:35:39 +0200 wenzelm some shortcuts for chunks, which sometimes avoid bulky string output;
Tue, 18 Mar 2014 17:39:03 +0100 wenzelm clarifed module name;
Thu, 27 Feb 2014 17:39:20 +0100 wenzelm modernized theory setup;
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;
Tue, 09 Apr 2013 15:29:25 +0200 wenzelm discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
Tue, 08 Jan 2013 22:10:02 +0100 wenzelm disable interactive mode of Specification.theorem with its slow printing of results;
Wed, 19 Sep 2012 14:47:15 +0200 wenzelm made SML/NJ happy;
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;
Fri, 29 Jun 2012 09:45:48 +0200 berghofe Various improvements
Wed, 21 Mar 2012 21:06:31 +0100 wenzelm optional 'includes' element for long theorem statements;
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
Tue, 28 Feb 2012 11:10:09 +0100 berghofe Added infrastructure for mapping SPARK field / constructor names
Fri, 08 Jul 2011 14:37:19 +0200 wenzelm more abstract Thy_Load.load_file/use_file for external theory resources;
Sat, 25 Jun 2011 17:17:49 +0200 wenzelm clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
Mon, 18 Apr 2011 16:33:45 +0200 berghofe Package prefix is now taken into account when looking up user-defined
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Fri, 15 Apr 2011 15:33:57 +0200 berghofe Added command for associating user-defined types with SPARK types.
Sun, 20 Mar 2011 17:40:45 +0100 wenzelm replaced File.check by specific File.check_file, File.check_dir;
Sun, 13 Mar 2011 16:38:54 +0100 wenzelm more basic use of Path.position/File.read;
Fri, 04 Mar 2011 17:39:30 +0100 berghofe spark_end now joins proofs of VCs before writing *.prv file.
Thu, 03 Mar 2011 18:42:12 +0100 wenzelm simplified Thy_Info.check_file -- discontinued load path;
Sun, 16 Jan 2011 17:21:13 +0100 berghofe Tuned show_status
Sun, 16 Jan 2011 15:04:16 +0100 wenzelm more standard command descriptions;
Sat, 15 Jan 2011 12:35:29 +0100 berghofe Added new SPARK verification environment.
less more (0) tip