| Sat, 30 Mar 2013 13:40:19 +0100 |
wenzelm |
more item markup;
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 16:38:25 +0100 |
wenzelm |
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 14:19:18 +0100 |
wenzelm |
tuned signature and module arrangement;
|
file |
diff |
annotate
|
| Sat, 09 Mar 2013 13:01:24 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 04 Mar 2013 15:03:46 +0100 |
wenzelm |
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 21:11:07 +0100 |
wenzelm |
simplified Proof.future_proof;
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 11:40:30 +0100 |
wenzelm |
proper check of Proof.is_relevant (again, cf. c3e99efacb67 and df8fc0567a3d);
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 17:55:26 +0100 |
wenzelm |
improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);
|
file |
diff |
annotate
|
| Fri, 25 Jan 2013 13:09:34 +0100 |
wenzelm |
clarified notion of Command.proper_range (according to Token.is_proper), especially relevant for Active.try_replace_command, to avoid loosing subsequent comments accidentally;
|
file |
diff |
annotate
|
| Wed, 16 Jan 2013 18:43:59 +0100 |
wenzelm |
proper range position;
|
file |
diff |
annotate
|
| Mon, 14 Jan 2013 13:59:43 +0100 |
wenzelm |
restrict "bad" markup to command keyword, notably excluding subsequent comments;
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 14:44:00 +0100 |
wenzelm |
recovered error to finish proof (e.g. bad obtain export) from 223f18cfbb32;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 14:15:46 +0200 |
wenzelm |
more robust future_proof result with specific error message (e.g. relevant for incomplete proof of non-registered theorem);
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 13:26:49 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 12:26:30 +0200 |
wenzelm |
avoid spurious "bad" markup for show/test_proof;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2012 14:20:54 +0200 |
wenzelm |
skipped proofs appear as "bad" without counting as error;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2012 13:20:08 +0200 |
wenzelm |
more method position information, notably finished_pos after end of previous text;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 20:35:24 +0200 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 20:23:00 +0200 |
wenzelm |
more proof method text position information;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 17:47:23 +0200 |
wenzelm |
clarified defer/prefer: more specific errors;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 15:14:12 +0200 |
wenzelm |
more informative errors for 'proof' and 'apply' steps;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 14:14:37 +0200 |
wenzelm |
more informative error for stand-alone 'qed';
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 14:02:02 +0200 |
wenzelm |
further attempts to unify/simplify goal output;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 13:06:40 +0200 |
wenzelm |
more informative error messages of initial/terminal proof methods;
|
file |
diff |
annotate
|
| Sat, 13 Oct 2012 21:09:20 +0200 |
wenzelm |
more informative error of initial/terminal proof steps;
|
file |
diff |
annotate
|
| Sat, 13 Oct 2012 19:53:04 +0200 |
wenzelm |
some attempts to unify/simplify pretty_goal;
|
file |
diff |
annotate
|
| Sat, 13 Oct 2012 18:04:11 +0200 |
wenzelm |
refined Proof.the_finished_goal with more informative error;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2012 20:05:17 +0200 |
wenzelm |
clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2012 19:46:21 +0200 |
wenzelm |
removed unused material;
|
file |
diff |
annotate
|