Tue, 17 Sep 2024 17:51:55 +0200 |
wenzelm |
more explicit context for syn_ext/mixfix operations, but it often degenerates to background theory;
|
file |
diff |
annotate
|
Thu, 12 Sep 2024 19:52:01 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Thu, 12 Sep 2024 15:09:07 +0200 |
wenzelm |
clarified signature: more explicit operations;
|
file |
diff |
annotate
|
Thu, 05 Sep 2024 17:39:45 +0200 |
wenzelm |
clarified signature: type ML_Pretty.pretty coincides with PolyML.pretty;
|
file |
diff |
annotate
|
Sat, 02 Dec 2023 15:42:50 +0100 |
wenzelm |
pro-forma support for optional zproof: no proper content yet;
|
file |
diff |
annotate
|
Mon, 25 Sep 2023 18:45:41 +0200 |
wenzelm |
clarified signature: avoid association with potentially dangerous Exn.capture;
|
file |
diff |
annotate
|
Wed, 26 Jul 2023 20:15:31 +0200 |
wenzelm |
prefer Output.writeln for theory "results", as opposed to Output.state for genuine proof states (see f8c412a45af8, c668735fb8b5, ecf80e37ed1a);
|
file |
diff |
annotate
|
Sat, 20 May 2023 17:42:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 22 Apr 2023 21:00:24 +0200 |
wenzelm |
tuned: concise combinators instead of bulky case-expressions;
|
file |
diff |
annotate
|
Thu, 08 Sep 2022 13:16:46 +0200 |
wenzelm |
removed odd TODO item (see 3391a493f39a);
|
file |
diff |
annotate
|
Thu, 08 Sep 2022 13:13:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 07 Sep 2022 21:15:45 +0200 |
wenzelm |
print goal instantiation for global qed (and variations);
|
file |
diff |
annotate
|
Mon, 05 Sep 2022 21:13:29 +0200 |
wenzelm |
show goal instantiation, notably for 'schematic_goal' command (inactive by default);
|
file |
diff |
annotate
|
Mon, 05 Sep 2022 19:23:12 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Mon, 05 Sep 2022 17:53:45 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Mon, 05 Sep 2022 13:32:09 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 05 Sep 2022 11:36:41 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 03 Sep 2022 17:37:46 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 13 Oct 2021 13:21:09 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Thu, 19 Sep 2019 15:09:12 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Wed, 18 Sep 2019 22:46:01 +0200 |
wenzelm |
support soft types for 'have' etc., with careful export wrt. result text to avoid extra assumptions (details may differ due to polymorphism);
|
file |
diff |
annotate
|
Wed, 18 Sep 2019 21:35:21 +0200 |
wenzelm |
proper export of result_text for 'have';
|
file |
diff |
annotate
|
Wed, 18 Sep 2019 20:53:53 +0200 |
wenzelm |
support soft types for 'assume';
|
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
|
Tue, 17 Sep 2019 17:06:05 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Tue, 17 Sep 2019 16:26:57 +0200 |
wenzelm |
clarified signature -- removed unused option (see acb0807ddb56);
|
file |
diff |
annotate
|
Tue, 13 Aug 2019 10:27:21 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|
Tue, 23 Jul 2019 12:07:50 +0200 |
wenzelm |
proof terms are always constructed sequentially;
|
file |
diff |
annotate
|
Tue, 16 Jul 2019 15:39:32 +0200 |
wenzelm |
support for a soft-type system within the Isabelle logical framework;
|
file |
diff |
annotate
|
Mon, 03 Jun 2019 15:40:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Sun, 23 Sep 2018 21:49:31 +0200 |
wenzelm |
discontinued old-style goal cases;
|
file |
diff |
annotate
|
Sun, 02 Sep 2018 19:48:15 +0200 |
wenzelm |
clarified reset_notepad;
|
file |
diff |
annotate
|
Sun, 02 Sep 2018 13:53:55 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Fri, 31 Aug 2018 22:25:58 +0200 |
wenzelm |
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
|
file |
diff |
annotate
|
Wed, 09 May 2018 20:45:57 +0200 |
wenzelm |
clarified future scheduling parameters, with support for parallel_limit;
|
file |
diff |
annotate
|
Fri, 23 Mar 2018 16:07:20 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Sun, 25 Feb 2018 15:44:46 +0100 |
wenzelm |
eliminated ASCII syntax from Pure bootstrap;
|
file |
diff |
annotate
|
Fri, 23 Feb 2018 20:55:46 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sun, 28 Jan 2018 19:28:52 +0100 |
wenzelm |
clarified take/drop/chop prefix/suffix;
|
file |
diff |
annotate
|
Fri, 08 Dec 2017 14:39:52 +0100 |
wenzelm |
implicit quick_and_dirty as for Toplevel.begin_proof/Proof.global_skip_proof;
|
file |
diff |
annotate
|
Thu, 07 Dec 2017 19:36:48 +0100 |
wenzelm |
clarified document preparation vs. skip_proofs;
|
file |
diff |
annotate
|
Sun, 03 Dec 2017 13:22:09 +0100 |
wenzelm |
discontinued old 'def' command;
|
file |
diff |
annotate
|
Mon, 10 Apr 2017 21:05:31 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 14 Dec 2016 16:59:41 +0100 |
wenzelm |
always close derivation, for significantly improved performance without parallel proofs;
|
file |
diff |
annotate
|
Thu, 27 Oct 2016 20:41:06 +0200 |
wenzelm |
avoid multiple PIDE markup due to (potentially infinite) backtracking;
|
file |
diff |
annotate
|
Fri, 22 Jul 2016 11:01:10 +0200 |
wenzelm |
more markup for unstructured calculation;
|
file |
diff |
annotate
|
Wed, 13 Jul 2016 15:23:33 +0200 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
Tue, 05 Jul 2016 14:20:27 +0200 |
wenzelm |
PIDE reports of implicit variable scope;
|
file |
diff |
annotate
|
Mon, 04 Jul 2016 19:08:54 +0200 |
wenzelm |
clarified fact position, notably for reports on literal facts;
|
file |
diff |
annotate
|
Mon, 04 Jul 2016 14:51:19 +0200 |
wenzelm |
more accurate facts index;
|
file |
diff |
annotate
|
Mon, 04 Jul 2016 10:29:56 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 22 Jun 2016 10:40:53 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Tue, 07 Jun 2016 19:55:45 +0200 |
wenzelm |
clean facts more uniformly;
|
file |
diff |
annotate
|
Tue, 07 Jun 2016 11:27:01 +0200 |
wenzelm |
tuned;
|
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
|
Mon, 25 Apr 2016 16:54:48 +0200 |
wenzelm |
clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
|
file |
diff |
annotate
|
Sun, 24 Apr 2016 21:31:14 +0200 |
wenzelm |
added Isar command 'define';
|
file |
diff |
annotate
|
Sun, 17 Apr 2016 20:11:02 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Fri, 15 Apr 2016 15:08:43 +0200 |
wenzelm |
clarified PIDE reports;
|
file |
diff |
annotate
|
Tue, 12 Apr 2016 14:50:53 +0200 |
wenzelm |
back to static Mixfix.default_constraint without any special tricks (reverting e6443edaebff);
|
file |
diff |
annotate
|
Sat, 02 Apr 2016 21:10:07 +0200 |
wenzelm |
careful export of type-dependent functions, without losing their special status;
|
file |
diff |
annotate
|
Wed, 30 Mar 2016 23:32:50 +0200 |
wenzelm |
more explicit support for object-logic constraint;
|
file |
diff |
annotate
|
Wed, 30 Mar 2016 22:00:55 +0200 |
wenzelm |
more accurate mixfix type constraints;
|
file |
diff |
annotate
|
Fri, 18 Mar 2016 16:26:35 +0100 |
wenzelm |
clarified modules;
|
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 17:48:33 +0100 |
wenzelm |
preserve names of for-fixes for faithfully;
|
file |
diff |
annotate
|
Fri, 13 Nov 2015 14:11:54 +0100 |
wenzelm |
avoid vacuous quantification, as usual for shared variable scope;
|
file |
diff |
annotate
|
Fri, 13 Nov 2015 11:41:11 +0100 |
wenzelm |
support for structure statements in 'assume', 'presume';
|
file |
diff |
annotate
|
Fri, 23 Oct 2015 17:17:11 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
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";
|
file |
diff |
annotate
|
Sun, 16 Aug 2015 18:19:30 +0200 |
wenzelm |
prefer theory_id operations;
|
file |
diff |
annotate
|
Tue, 28 Jul 2015 20:05:53 +0200 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
Tue, 14 Jul 2015 19:01:46 +0200 |
wenzelm |
more aggressive compaction of multi-goal proof terms (see also a8babbb6d5ea, 4dd0ba632e40);
|
file |
diff |
annotate
|
Wed, 01 Jul 2015 21:29:57 +0200 |
wenzelm |
support for subgoal focus command;
|
file |
diff |
annotate
|
Tue, 30 Jun 2015 15:20:56 +0200 |
wenzelm |
renamed "default" to "standard", to make semantically clear what it is;
|
file |
diff |
annotate
|
Mon, 29 Jun 2015 21:56:20 +0200 |
wenzelm |
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
|
file |
diff |
annotate
|
Sat, 27 Jun 2015 00:10:24 +0200 |
wenzelm |
premises in 'show' are treated like 'assume';
|
file |
diff |
annotate
|
Thu, 25 Jun 2015 12:10:07 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 24 Jun 2015 21:26:03 +0200 |
wenzelm |
clarified 'case' command;
|
file |
diff |
annotate
|
Mon, 22 Jun 2015 20:36:33 +0200 |
wenzelm |
support 'when' statement, which corresponds to 'presume';
|
file |
diff |
annotate
|
Mon, 22 Jun 2015 16:48:27 +0200 |
wenzelm |
clarified nesting of Isar goal structure;
|
file |
diff |
annotate
|
Mon, 22 Jun 2015 11:35:30 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 14 Jun 2015 15:53:13 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 13 Jun 2015 23:36:21 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 13 Jun 2015 13:09:05 +0200 |
wenzelm |
renamed "prems" to "that";
|
file |
diff |
annotate
|
Thu, 11 Jun 2015 16:15:27 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
Wed, 10 Jun 2015 18:48:48 +0200 |
wenzelm |
prefer direct Assumption.add_assms -- avoid term bindings of Proof_Context.add_assms;
|
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
|
Wed, 10 Jun 2015 11:14:04 +0200 |
wenzelm |
no need for protected goal (see 240ad53041c9);
|
file |
diff |
annotate
|
Wed, 10 Jun 2015 10:29:32 +0200 |
wenzelm |
prevent export of future result -- avoid interference with goal fixes;
|
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 12:32:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Tue, 09 Jun 2015 12:17:50 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 09 Jun 2015 11:51:05 +0200 |
wenzelm |
clarified term bindings;
|
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 14:45:31 +0200 |
wenzelm |
tuned signature;
|
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
|
Fri, 05 Jun 2015 13:41:06 +0200 |
wenzelm |
added Isar command 'supply';
|
file |
diff |
annotate
|
Fri, 05 Jun 2015 11:11:26 +0200 |
wenzelm |
clarified signature -- better support for Isar commands outside of Pure;
|
file |
diff |
annotate
|
Thu, 16 Apr 2015 14:18:32 +0200 |
wenzelm |
explicit error for Toplevel.proof_of;
|
file |
diff |
annotate
|
Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
Wed, 08 Apr 2015 11:52:53 +0200 |
wenzelm |
tuned signature;
|
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
|
Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
Sun, 01 Mar 2015 23:35:41 +0100 |
wenzelm |
added Proof_Context.cterm_of/ctyp_of convenience;
|
file |
diff |
annotate
|
Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
Tue, 23 Dec 2014 21:04:53 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
Tue, 23 Dec 2014 20:46:42 +0100 |
wenzelm |
explicit message channels for "state", "information";
|
file |
diff |
annotate
|
Fri, 19 Dec 2014 12:36:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|