src/Pure/Isar/obtain.ML
Sun, 25 Feb 2018 15:44:46 +0100 wenzelm eliminated ASCII syntax from Pure bootstrap;
Thu, 23 Jun 2016 11:01:14 +0200 wenzelm tuned signature;
Tue, 26 Apr 2016 22:39:17 +0200 wenzelm 'obtain' supports structured statements (similar to 'define');
Tue, 26 Apr 2016 19:37:47 +0200 wenzelm more uniform operations for structured statements;
Tue, 26 Apr 2016 16:20:28 +0200 wenzelm defs are closed, which leads to proper auto_bind_facts;
Sun, 24 Apr 2016 20:29:49 +0200 wenzelm clarified modules;
Mon, 18 Apr 2016 20:24:19 +0200 wenzelm prefer internal attribute source;
Sun, 13 Dec 2015 21:56:15 +0100 wenzelm more general types Proof.method / context_tactic;
Fri, 13 Nov 2015 11:41:11 +0100 wenzelm support for structure statements in 'assume', 'presume';
Fri, 25 Sep 2015 20:37:59 +0200 wenzelm moved remaining display.ML to more_thm.ML;
Sun, 16 Aug 2015 19:25:08 +0200 wenzelm added Thm.chyps_of;
Wed, 08 Jul 2015 19:28:43 +0200 wenzelm Variable.focus etc.: optional bindings provided by user;
Sun, 05 Jul 2015 15:02:30 +0200 wenzelm simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
Mon, 22 Jun 2015 20:36:33 +0200 wenzelm support 'when' statement, which corresponds to 'presume';
Mon, 15 Jun 2015 10:33:37 +0200 wenzelm more robust: variables need not occur in body;
Sun, 14 Jun 2015 23:22:08 +0200 wenzelm improved treatment of Element.Obtains via Expression.prepare_stmt;
Sun, 14 Jun 2015 19:15:31 +0200 wenzelm tuned comment;
Sat, 13 Jun 2015 23:36:21 +0200 wenzelm tuned signature;
Sat, 13 Jun 2015 19:38:26 +0200 wenzelm open parameters for 'consider' rule;
Sat, 13 Jun 2015 16:35:27 +0200 wenzelm eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
Sat, 13 Jun 2015 15:51:19 +0200 wenzelm clarified 'obtain', using structured 'have' statement;
Sat, 13 Jun 2015 15:16:59 +0200 wenzelm tuned comments;
Sat, 13 Jun 2015 14:37:50 +0200 wenzelm clarified 'consider', using structured 'have' statement;
Thu, 11 Jun 2015 22:47:53 +0200 wenzelm support for 'consider' command;
Thu, 11 Jun 2015 15:44:00 +0200 wenzelm support to parse obtain clause without type-checking yet;
Thu, 11 Jun 2015 10:44:04 +0200 wenzelm tuned signature;
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;
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 13:42:58 +0200 wenzelm clarified abstracted term bindings (again, see c8384ff11711);
Tue, 09 Jun 2015 11:51:05 +0200 wenzelm clarified term bindings;
Mon, 08 Jun 2015 22:04:15 +0200 wenzelm clarified context;
Mon, 08 Jun 2015 21:39:16 +0200 wenzelm tuned;
Mon, 08 Jun 2015 21:23:28 +0200 wenzelm clarified abstracted term bindings;
Mon, 08 Jun 2015 20:58:43 +0200 wenzelm avoid duplicate warning due to Variable.warn_extra_tfrees;
Mon, 08 Jun 2015 20:53:42 +0200 wenzelm clarified Proof_Context.cert_propp/read_propp;
Mon, 08 Jun 2015 19:38:08 +0200 wenzelm more careful treatment of term bindings in 'obtain' proof body;
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;
Sat, 30 May 2015 21:52:37 +0200 wenzelm more explicit context;
Wed, 08 Apr 2015 19:39:08 +0200 wenzelm proper context for Object_Logic operations;
Fri, 06 Mar 2015 17:32:20 +0100 wenzelm clarified context;
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;
Sun, 01 Mar 2015 23:35:41 +0100 wenzelm added Proof_Context.cterm_of/ctyp_of convenience;
Fri, 09 May 2014 22:04:50 +0200 wenzelm more position markup to help locating the query context, e.g. from "Info" dockable;
Wed, 07 May 2014 13:55:16 +0200 wenzelm print results as "state", to avoid intrusion into the source text;
Tue, 31 Dec 2013 14:29:16 +0100 wenzelm proper context for norm_hhf and derived operations;
Wed, 26 Jun 2013 11:54:45 +0200 wenzelm tuned signature;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Sat, 29 Sep 2012 18:23:46 +0200 wenzelm more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
Fri, 27 Apr 2012 22:47:30 +0200 wenzelm clarified signature;
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);
Sat, 14 Jan 2012 21:16:15 +0100 wenzelm discontinued old-style Term.list_abs in favour of plain Term.abs;
Sat, 14 Jan 2012 17:45:04 +0100 wenzelm discontinued old-style Term.list_all_free in favour of plain Logic.all;
Mon, 07 Nov 2011 17:00:23 +0100 wenzelm tuned signature -- avoid spurious Thm.mixed_attribute;
less more (0) -100 -60 tip