| Sun, 26 Sep 2021 18:49:55 +0200 |
wenzelm |
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 14:50:26 +0200 |
wenzelm |
clarified set of items with order of addition;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 12:33:14 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 21:25:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 18:21:58 +0200 |
wenzelm |
more scalable operations;
|
file |
diff |
annotate
|
| Thu, 19 Sep 2019 15:09:12 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 18 Sep 2019 20:10:15 +0200 |
wenzelm |
more robust declaration of resulting statement text, instead of somewhat accidental (Variable.maybe_bind_term result_binds in generic_goal);
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 15:44:46 +0100 |
wenzelm |
eliminated ASCII syntax from Pure bootstrap;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2016 22:39:17 +0200 |
wenzelm |
'obtain' supports structured statements (similar to 'define');
|
file |
diff |
annotate
|
| Tue, 26 Apr 2016 19:37:47 +0200 |
wenzelm |
more uniform operations for structured statements;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2016 16:20:28 +0200 |
wenzelm |
defs are closed, which leads to proper auto_bind_facts;
|
file |
diff |
annotate
|
| Sun, 24 Apr 2016 20:29:49 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 20:24:19 +0200 |
wenzelm |
prefer internal attribute source;
|
file |
diff |
annotate
|
| Sun, 13 Dec 2015 21:56:15 +0100 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2015 11:41:11 +0100 |
wenzelm |
support for structure statements in 'assume', 'presume';
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 19:25:08 +0200 |
wenzelm |
added Thm.chyps_of;
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 19:28:43 +0200 |
wenzelm |
Variable.focus etc.: optional bindings provided by user;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Mon, 22 Jun 2015 20:36:33 +0200 |
wenzelm |
support 'when' statement, which corresponds to 'presume';
|
file |
diff |
annotate
|
| Mon, 15 Jun 2015 10:33:37 +0200 |
wenzelm |
more robust: variables need not occur in body;
|
file |
diff |
annotate
|
| Sun, 14 Jun 2015 23:22:08 +0200 |
wenzelm |
improved treatment of Element.Obtains via Expression.prepare_stmt;
|
file |
diff |
annotate
|
| Sun, 14 Jun 2015 19:15:31 +0200 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 23:36:21 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 19:38:26 +0200 |
wenzelm |
open parameters for 'consider' rule;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 16:35:27 +0200 |
wenzelm |
eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 15:51:19 +0200 |
wenzelm |
clarified 'obtain', using structured 'have' statement;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 15:16:59 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 14:37:50 +0200 |
wenzelm |
clarified 'consider', using structured 'have' statement;
|
file |
diff |
annotate
|
| Thu, 11 Jun 2015 22:47:53 +0200 |
wenzelm |
support for 'consider' command;
|
file |
diff |
annotate
|
| Thu, 11 Jun 2015 15:44:00 +0200 |
wenzelm |
support to parse obtain clause without type-checking yet;
|
file |
diff |
annotate
|
| Thu, 11 Jun 2015 10:44:04 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 16:09:49 +0200 |
wenzelm |
clarified local after_qed: result is not exported yet;
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 14:46:31 +0200 |
wenzelm |
support for "if prems" in local goal statements;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 22:24:33 +0200 |
wenzelm |
more uniform treatment of auto bindings vs. explicit user bindings;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 16:42:17 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 16:07:11 +0200 |
wenzelm |
allow for_fixes for 'have', 'show' etc.;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 13:42:58 +0200 |
wenzelm |
clarified abstracted term bindings (again, see c8384ff11711);
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 11:51:05 +0200 |
wenzelm |
clarified term bindings;
|
file |
diff |
annotate
|
| Mon, 08 Jun 2015 22:04:15 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Mon, 08 Jun 2015 21:39:16 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 08 Jun 2015 21:23:28 +0200 |
wenzelm |
clarified abstracted term bindings;
|
file |
diff |
annotate
|
| Mon, 08 Jun 2015 20:58:43 +0200 |
wenzelm |
avoid duplicate warning due to Variable.warn_extra_tfrees;
|
file |
diff |
annotate
|
| Mon, 08 Jun 2015 20:53:42 +0200 |
wenzelm |
clarified Proof_Context.cert_propp/read_propp;
|
file |
diff |
annotate
|
| Mon, 08 Jun 2015 19:38:08 +0200 |
wenzelm |
more careful treatment of term bindings in 'obtain' proof body;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 23:37:32 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 21:58:18 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 20:03:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 15:01:07 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 30 May 2015 21:52:37 +0200 |
wenzelm |
more explicit context;
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 17:32:20 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 13:28:04 +0100 |
wenzelm |
tuned -- more explicit use of context;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2015 23:35:41 +0100 |
wenzelm |
added Proof_Context.cterm_of/ctyp_of convenience;
|
file |
diff |
annotate
|
| Fri, 09 May 2014 22:04:50 +0200 |
wenzelm |
more position markup to help locating the query context, e.g. from "Info" dockable;
|
file |
diff |
annotate
|
| Wed, 07 May 2014 13:55:16 +0200 |
wenzelm |
print results as "state", to avoid intrusion into the source text;
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
| Wed, 26 Jun 2013 11:54:45 +0200 |
wenzelm |
tuned signature;
|
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
|
| 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;
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 22:47:30 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 21:16:15 +0100 |
wenzelm |
discontinued old-style Term.list_abs in favour of plain Term.abs;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 17:45:04 +0100 |
wenzelm |
discontinued old-style Term.list_all_free in favour of plain Logic.all;
|
file |
diff |
annotate
|
| Mon, 07 Nov 2011 17:00:23 +0100 |
wenzelm |
tuned signature -- avoid spurious Thm.mixed_attribute;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 23:55:53 +0100 |
wenzelm |
more general Proof_Context.bind_propp, which allows outer parameters;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 22:51:37 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 22:23:41 +0100 |
wenzelm |
tuned signature -- canonical argument order;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2011 20:20:49 +0200 |
wenzelm |
eliminated slightly odd Proof_Context.bind_fixes;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 23:02:43 +0200 |
wenzelm |
more precise positions via binding;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 21:50:04 +0200 |
wenzelm |
clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 20:58:40 +0200 |
wenzelm |
tuned signature -- eliminated odd comment;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 19:55:42 +0200 |
wenzelm |
more formal treatment of parameters, avoiding slightly odd Variable.intern_fixed;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 17:58:45 +0200 |
wenzelm |
reorganized fixes as specialized (global) name space;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 12:46:18 +0200 |
wenzelm |
tuned signature, disentangled dependencies;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:08:56 +0100 |
wenzelm |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 21:41:24 +0200 |
wenzelm |
turned show_sorts/show_types into proper configuration options;
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 15:19:39 +0200 |
wenzelm |
tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 15:52:03 +0200 |
wenzelm |
modernized naming conventions of main Isar proof elements;
|
file |
diff |
annotate
|
| Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:57:48 +0100 |
wenzelm |
modernized structure Proof_Display;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:45:23 +0100 |
wenzelm |
modernized structure AutoBind;
|
file |
diff |
annotate
|
| Sun, 01 Nov 2009 15:44:26 +0100 |
wenzelm |
modernized structure Context_Rules;
|
file |
diff |
annotate
|
| Sun, 01 Nov 2009 15:24:45 +0100 |
wenzelm |
modernized structure Rule_Cases;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 15:57:51 +0200 |
wenzelm |
indicate CRITICAL nature of various setmp combinators;
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 22:25:50 +0200 |
wenzelm |
eliminated dead code;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2009 13:12:54 +0200 |
wenzelm |
Variable.focus: named parameters;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 01:03:18 +0200 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
| Wed, 24 Jun 2009 21:28:02 +0200 |
wenzelm |
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 17:53:33 +0100 |
wenzelm |
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 16:31:16 +0100 |
wenzelm |
replaced add_binds(_i) by bind_terms -- internal version only;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 13:28:55 +0100 |
wenzelm |
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 18:32:01 +0100 |
wenzelm |
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 14:07:43 +0100 |
wenzelm |
Thm.binding;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:32 +0100 |
haftmann |
binding is alias for Binding.T
|
file |
diff |
annotate
|
| Wed, 07 Jan 2009 16:22:10 +0100 |
wenzelm |
qed/after_qed: singleton result;
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 18:43:42 +0100 |
haftmann |
Name.name_of -> Binding.base_name
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 16:55:33 +0200 |
wenzelm |
type Attrib.binding abbreviates Name.binding without attributes;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:30 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2007 19:24:13 +0200 |
wenzelm |
renamed Variable.import to import_thms (avoid clash with Alice keywords);
|
file |
diff |
annotate
|
| Wed, 06 Dec 2006 21:19:03 +0100 |
wenzelm |
export: added explicit term operation;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 14:17:29 +0100 |
wenzelm |
qualified MetaSimplifier.norm_hhf(_protect);
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 19:39:50 +0100 |
wenzelm |
moved statement to specification.ML;
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 21:39:31 +0200 |
wenzelm |
statement: Variable.fix_frees;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:27:02 +0200 |
wenzelm |
added tactical result;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:43:01 +0200 |
wenzelm |
moved basic assumption operations from structure ProofContext to Assumption;
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:37:41 +0200 |
wenzelm |
Variable.import(T): result includes fixed types/terms;
|
file |
diff |
annotate
|