| Fri, 25 Jan 2013 13:09:34 +0100 |
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 |
proper range position;
|
file | diff | annotate |
| Mon, 14 Jan 2013 13:59:43 +0100 |
restrict "bad" markup to command keyword, notably excluding subsequent comments;
|
file | diff | annotate |
| Mon, 03 Dec 2012 14:44:00 +0100 |
recovered error to finish proof (e.g. bad obtain export) from 223f18cfbb32;
|
file | diff | annotate |
| Sun, 25 Nov 2012 19:49:24 +0100 |
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 |
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 |
tuned message;
|
file | diff | annotate |
| Thu, 18 Oct 2012 12:26:30 +0200 |
avoid spurious "bad" markup for show/test_proof;
|
file | diff | annotate |
| Wed, 17 Oct 2012 14:20:54 +0200 |
skipped proofs appear as "bad" without counting as error;
|
file | diff | annotate |
| Wed, 17 Oct 2012 13:20:08 +0200 |
more method position information, notably finished_pos after end of previous text;
|
file | diff | annotate |
| Tue, 16 Oct 2012 20:35:24 +0200 |
tuned messages;
|
file | diff | annotate |
| Tue, 16 Oct 2012 20:23:00 +0200 |
more proof method text position information;
|
file | diff | annotate |
| Tue, 16 Oct 2012 17:47:23 +0200 |
clarified defer/prefer: more specific errors;
|
file | diff | annotate |
| Tue, 16 Oct 2012 15:14:12 +0200 |
more informative errors for 'proof' and 'apply' steps;
|
file | diff | annotate |
| Tue, 16 Oct 2012 14:14:37 +0200 |
more informative error for stand-alone 'qed';
|
file | diff | annotate |
| Tue, 16 Oct 2012 14:02:02 +0200 |
further attempts to unify/simplify goal output;
|
file | diff | annotate |
| Tue, 16 Oct 2012 13:06:40 +0200 |
more informative error messages of initial/terminal proof methods;
|
file | diff | annotate |
| Sat, 13 Oct 2012 21:09:20 +0200 |
more informative error of initial/terminal proof steps;
|
file | diff | annotate |
| Sat, 13 Oct 2012 19:53:04 +0200 |
some attempts to unify/simplify pretty_goal;
|
file | diff | annotate |
| Sat, 13 Oct 2012 18:04:11 +0200 |
refined Proof.the_finished_goal with more informative error;
|
file | diff | annotate |
| Tue, 09 Oct 2012 20:05:17 +0200 |
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 |
removed unused material;
|
file | diff | annotate |
| Sat, 01 Sep 2012 19:43:18 +0200 |
discontinued complicated/unreliable notion of recent proofs within context;
|
file | diff | annotate |
| Fri, 31 Aug 2012 16:35:30 +0200 |
more precise register_proofs for local goals;
|
file | diff | annotate |
| Thu, 30 Aug 2012 21:50:49 +0200 |
register proofs of Isar goals, to enable recovery from unstable command states after interactive cancellation;
|
file | diff | annotate |
| Thu, 30 Aug 2012 21:23:04 +0200 |
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
|
file | diff | annotate |
| Thu, 30 Aug 2012 19:18:49 +0200 |
some support for registering forked proofs within Proof.state, using its bottom context;
|
file | diff | annotate |
| Fri, 27 Apr 2012 22:47:30 +0200 |
clarified signature;
|
file | diff | annotate |
| Thu, 12 Apr 2012 11:34:50 +0200 |
more precise declaration of goal_tfrees in forked proof state;
|
file | diff | annotate |
| Tue, 10 Apr 2012 21:31:05 +0200 |
static relevance of proof via syntax keywords;
|
file | diff | annotate |
| Wed, 21 Mar 2012 21:24:13 +0100 |
tuned signature;
|
file | diff | annotate |
| Wed, 21 Mar 2012 17:16:39 +0100 |
tuned messages;
|
file | diff | annotate |
| Wed, 21 Mar 2012 11:00:34 +0100 |
prefer explicitly qualified exception List.Empty;
|
file | diff | annotate |
| Sun, 18 Mar 2012 13:04:22 +0100 |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file | diff | annotate |
| Tue, 28 Feb 2012 16:43:32 +0100 |
display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
|
file | diff | annotate |
| Tue, 14 Feb 2012 19:51:39 +0100 |
tuned signature, according to actual usage of these operations;
|
file | diff | annotate |
| Mon, 28 Nov 2011 22:05:32 +0100 |
separate module for concrete Isabelle markup;
|
file | diff | annotate |
| Sun, 20 Nov 2011 16:59:37 +0100 |
uniform cert_vars/read_vars;
|
file | diff | annotate |
| Mon, 07 Nov 2011 17:00:23 +0100 |
tuned signature -- avoid spurious Thm.mixed_attribute;
|
file | diff | annotate |
| Thu, 03 Nov 2011 22:23:41 +0100 |
tuned signature -- canonical argument order;
|
file | diff | annotate |
| Mon, 01 Aug 2011 12:08:53 +0200 |
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
|
file | diff | annotate |
| Mon, 11 Jul 2011 22:55:47 +0200 |
tuned signature -- corresponding to Scala version;
|
file | diff | annotate |
| Thu, 12 May 2011 16:23:13 +0200 |
proper configuration options Proof_Context.debug and Proof_Context.verbose;
|
file | diff | annotate |
| Wed, 27 Apr 2011 23:02:43 +0200 |
more precise positions via binding;
|
file | diff | annotate |
| Sat, 16 Apr 2011 15:47:52 +0200 |
modernized structure Proof_Context;
|
file | diff | annotate |
| Fri, 08 Apr 2011 14:20:57 +0200 |
discontinued special treatment of structure Mixfix;
|
file | diff | annotate |
| Mon, 21 Mar 2011 20:15:03 +0100 |
tuned;
|
file | diff | annotate |
| Mon, 31 Jan 2011 23:53:07 +0100 |
more specific Goal.fork_name;
|
file | diff | annotate |
| Wed, 15 Dec 2010 20:52:20 +0100 |
show: display goal refinement rule as "state", to avoid odd Output.urgent_message and make its association with the goal more explicit;
|
file | diff | annotate |
| Sat, 04 Dec 2010 21:26:55 +0100 |
formal notepad without any result;
|
file | diff | annotate |
| Mon, 22 Nov 2010 10:42:04 +0100 |
added useful function map_context_result to signature
|
file | diff | annotate |
| Mon, 25 Oct 2010 21:06:56 +0200 |
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
|
file | diff | annotate |
| Wed, 22 Sep 2010 18:21:48 +0200 |
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
|
file | diff | annotate |
| Thu, 09 Sep 2010 17:20:27 +0200 |
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
|
file | diff | annotate |
| Sat, 04 Sep 2010 00:31:21 +0200 |
recovered options for goal antiquotations from f45d332a90e3: actually pass context to Proof.pretty_goals (see also 45facd8f358e);
|
file | diff | annotate |
| Fri, 03 Sep 2010 21:13:53 +0200 |
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
|
file | diff | annotate |
| Fri, 03 Sep 2010 11:27:35 +0200 |
Proof.pretty_state: print everything in the foreground context to give users a chance to configure options, e.g. via "using [[show_consts]]";
|
file | diff | annotate |
| Wed, 25 Aug 2010 21:31:22 +0200 |
added some proof state markup, notably number of subgoals (e.g. for indentation);
|
file | diff | annotate |
| Wed, 11 Aug 2010 17:37:04 +0200 |
removed obsolete Proof.get_thmss_cmd (cf. Attrib.eval_thms);
|
file | diff | annotate |
| Fri, 06 Aug 2010 14:35:04 +0200 |
removed obsolete Goal.local_future_enforced: Toplevel.run_command is no longer interactive, so Goal.local_future_enabled is sufficient (cf. 349e9223c685 and e07dacec79e7);
|
file | diff | annotate |