| Fri, 30 Dec 2011 13:52:07 +0100 |
wenzelm |
simplified proof;
|
file |
diff |
annotate
|
| Fri, 30 Dec 2011 12:54:55 +0100 |
wenzelm |
simplified proof;
|
file |
diff |
annotate
|
| Fri, 30 Dec 2011 12:12:16 +0100 |
wenzelm |
more parallelism;
|
file |
diff |
annotate
|
| Fri, 30 Dec 2011 12:00:10 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 20:31:58 +0100 |
wenzelm |
tuned -- afford slightly larger simpset in simp_defs_tac;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 20:05:53 +0100 |
wenzelm |
tuned -- standard proofs by default;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 18:27:17 +0100 |
wenzelm |
clarified timeit_msg;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 16:58:19 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 20:10:28 +0100 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 15:23:27 +0100 |
wenzelm |
eliminated some legacy operations;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 14:54:25 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
adapting exhaustive generators in record package
|
file |
diff |
annotate
|
| Wed, 23 Nov 2011 22:59:39 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2011 11:02:06 +0100 |
wenzelm |
simultaneous check;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 17:57:42 +0100 |
wenzelm |
sort assignment before simultaneous term_check, not isolated parse_term;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 15:18:39 +0100 |
wenzelm |
localized Record.decode_type: use standard Proof_Context.get_sort;
|
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
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| Wed, 06 Jul 2011 22:02:52 +0200 |
wenzelm |
clarified record syntax: fieldext excludes the "more" pseudo-field (unlike 2f885b7e5ba7), so that errors like (| x = a, more = b |) are reported less confusingly;
|
file |
diff |
annotate
|
| Wed, 06 Jul 2011 20:14:13 +0200 |
wenzelm |
tuned errors;
|
file |
diff |
annotate
|
| Wed, 06 Jul 2011 13:31:12 +0200 |
wenzelm |
record package: proper configuration options;
|
file |
diff |
annotate
|
| Wed, 06 Jul 2011 11:37:29 +0200 |
wenzelm |
just one copy of split_args;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Fri, 13 May 2011 23:58:40 +0200 |
wenzelm |
clarified map_simpset versus Simplifier.map_simpset_global;
|
file |
diff |
annotate
|
| Fri, 13 May 2011 22:55:00 +0200 |
wenzelm |
proper Proof.context for classical tactics;
|
file |
diff |
annotate
|
| Thu, 05 May 2011 10:47:31 +0200 |
bulwahn |
adding creation of exhaustive generators for records; simplifying dependencies in Main theory
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 21:42:47 +0200 |
wenzelm |
added Binding.print convenience, which includes quote already;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|