src/Pure/Isar/proof.ML
Fri, 18 Mar 2016 16:26:35 +0100 wenzelm clarified modules;
Sun, 13 Dec 2015 21:56:15 +0100 wenzelm more general types Proof.method / context_tactic;
Fri, 13 Nov 2015 17:48:33 +0100 wenzelm preserve names of for-fixes for faithfully;
Fri, 13 Nov 2015 14:11:54 +0100 wenzelm avoid vacuous quantification, as usual for shared variable scope;
Fri, 13 Nov 2015 11:41:11 +0100 wenzelm support for structure statements in 'assume', 'presume';
Fri, 23 Oct 2015 17:17:11 +0200 wenzelm clarified modules;
Fri, 25 Sep 2015 20:37:59 +0200 wenzelm moved remaining display.ML to more_thm.ML;
Thu, 03 Sep 2015 19:27:45 +0200 wenzelm proper restore_naming after global qed, which is important to make Name_Space.transform_naming work properly, e.g. for "private typedef";
Sun, 16 Aug 2015 18:19:30 +0200 wenzelm prefer theory_id operations;
Tue, 28 Jul 2015 20:05:53 +0200 wenzelm proper context;
Tue, 14 Jul 2015 19:01:46 +0200 wenzelm more aggressive compaction of multi-goal proof terms (see also a8babbb6d5ea, 4dd0ba632e40);
Wed, 01 Jul 2015 21:29:57 +0200 wenzelm support for subgoal focus command;
Tue, 30 Jun 2015 15:20:56 +0200 wenzelm renamed "default" to "standard", to make semantically clear what it is;
Mon, 29 Jun 2015 21:56:20 +0200 wenzelm clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
Sat, 27 Jun 2015 00:10:24 +0200 wenzelm premises in 'show' are treated like 'assume';
Thu, 25 Jun 2015 12:10:07 +0200 wenzelm tuned signature;
Wed, 24 Jun 2015 21:26:03 +0200 wenzelm clarified 'case' command;
Mon, 22 Jun 2015 20:36:33 +0200 wenzelm support 'when' statement, which corresponds to 'presume';
Mon, 22 Jun 2015 16:48:27 +0200 wenzelm clarified nesting of Isar goal structure;
Mon, 22 Jun 2015 11:35:30 +0200 wenzelm tuned;
Sun, 14 Jun 2015 15:53:13 +0200 wenzelm tuned signature;
Sat, 13 Jun 2015 23:36:21 +0200 wenzelm tuned signature;
Sat, 13 Jun 2015 13:09:05 +0200 wenzelm renamed "prems" to "that";
Thu, 11 Jun 2015 16:15:27 +0200 wenzelm made SML/NJ happy;
Wed, 10 Jun 2015 18:48:48 +0200 wenzelm prefer direct Assumption.add_assms -- avoid term bindings of Proof_Context.add_assms;
Wed, 10 Jun 2015 16:09:49 +0200 wenzelm clarified local after_qed: result is not exported yet;
Wed, 10 Jun 2015 14:46:31 +0200 wenzelm support for "if prems" in local goal statements;
Wed, 10 Jun 2015 11:14:04 +0200 wenzelm no need for protected goal (see 240ad53041c9);
Wed, 10 Jun 2015 10:29:32 +0200 wenzelm prevent export of future result -- avoid interference with goal fixes;
Tue, 09 Jun 2015 22:24:33 +0200 wenzelm more uniform treatment of auto bindings vs. explicit user bindings;
Tue, 09 Jun 2015 16:42:17 +0200 wenzelm tuned signature;
Tue, 09 Jun 2015 16:07:11 +0200 wenzelm allow for_fixes for 'have', 'show' etc.;
Tue, 09 Jun 2015 12:32:01 +0200 wenzelm tuned signature;
Tue, 09 Jun 2015 12:17:50 +0200 wenzelm tuned;
Tue, 09 Jun 2015 11:51:05 +0200 wenzelm clarified term bindings;
Mon, 08 Jun 2015 20:53:42 +0200 wenzelm clarified Proof_Context.cert_propp/read_propp;
Mon, 08 Jun 2015 14:45:31 +0200 wenzelm tuned signature;
Sun, 07 Jun 2015 23:37:32 +0200 wenzelm tuned signature;
Sun, 07 Jun 2015 21:58:18 +0200 wenzelm tuned signature;
Sun, 07 Jun 2015 20:03:40 +0200 wenzelm tuned signature;
Sun, 07 Jun 2015 15:01:07 +0200 wenzelm tuned signature;
Fri, 05 Jun 2015 13:41:06 +0200 wenzelm added Isar command 'supply';
Fri, 05 Jun 2015 11:11:26 +0200 wenzelm clarified signature -- better support for Isar commands outside of Pure;
Thu, 16 Apr 2015 14:18:32 +0200 wenzelm explicit error for Toplevel.proof_of;
Wed, 08 Apr 2015 19:39:08 +0200 wenzelm proper context for Object_Logic operations;
Wed, 08 Apr 2015 11:52:53 +0200 wenzelm tuned signature;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Thu, 05 Mar 2015 13:28:04 +0100 wenzelm tuned -- more explicit use of context;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Sun, 01 Mar 2015 23:35:41 +0100 wenzelm added Proof_Context.cterm_of/ctyp_of convenience;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Tue, 23 Dec 2014 21:04:53 +0100 wenzelm tuned message;
Tue, 23 Dec 2014 20:46:42 +0100 wenzelm explicit message channels for "state", "information";
Fri, 19 Dec 2014 12:36:50 +0100 wenzelm tuned;
Sat, 08 Nov 2014 21:31:51 +0100 wenzelm optional proof context for unify operations, for the sake of proper local options;
Mon, 03 Nov 2014 14:31:15 +0100 wenzelm eliminated obsolete Proof.goal_message -- print outcome more directly;
Thu, 30 Oct 2014 16:20:46 +0100 wenzelm eliminated aliases;
Tue, 28 Oct 2014 10:35:38 +0100 wenzelm 'oops' requires proper goal statement -- exclude 'notepad' to avoid disrupting begin/end structure;
Tue, 28 Oct 2014 09:57:12 +0100 wenzelm more abstract type;
Tue, 28 Oct 2014 09:32:18 +0100 wenzelm tuned;
less more (0) -300 -100 -60 tip