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