| 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
|