src/Pure/Isar/specification.ML
Mon, 02 Dec 2019 16:28:23 +0100 wenzelm clarified name: avoid clashes;
Mon, 02 Dec 2019 15:04:38 +0100 wenzelm proper spec_rule name via naming/binding/Morphism.binding;
Mon, 02 Dec 2019 13:34:02 +0100 wenzelm more informative spec rules;
Fri, 29 Nov 2019 20:57:04 +0100 wenzelm more informative spec rules: optional name;
Thu, 19 Sep 2019 15:09:12 +0200 wenzelm clarified signature;
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);
Mon, 03 Jun 2019 15:40:08 +0200 wenzelm clarified signature;
Tue, 26 Mar 2019 22:13:36 +0100 wenzelm more informative Spec_Rules.Equational, notably primrec argument types;
Sun, 02 Jul 2017 20:13:38 +0200 haftmann proper concept of code declaration wrt. atomicity and Isar declarations
Mon, 03 Jul 2017 13:51:55 +0200 wenzelm added command 'alias' and 'type_alias';
Tue, 05 Jul 2016 20:51:02 +0200 wenzelm PIDE reports of implicit variable scope;
Tue, 05 Jul 2016 14:20:27 +0200 wenzelm PIDE reports of implicit variable scope;
Tue, 05 Jul 2016 10:32:25 +0200 wenzelm tuned;
Thu, 23 Jun 2016 11:01:14 +0200 wenzelm tuned signature;
Thu, 09 Jun 2016 12:02:38 +0200 wenzelm tuned signature;
Mon, 06 Jun 2016 21:28:46 +0200 haftmann explicit tagging of code equations de-baroquifies interface
Mon, 30 May 2016 14:15:44 +0200 wenzelm allow 'for' fixes for multi_specs;
Mon, 30 May 2016 11:44:41 +0200 wenzelm unused;
Sun, 29 May 2016 15:40:25 +0200 wenzelm clarified check_open_spec / read_open_spec;
Sat, 28 May 2016 23:55:41 +0200 wenzelm tuned;
Sat, 28 May 2016 21:38:58 +0200 wenzelm clarified 'axiomatization';
Sat, 14 May 2016 22:00:44 +0200 wenzelm re-enable fact index for 'obtains' assumption (amending 5c8e6a751adc);
Sat, 14 May 2016 19:49:10 +0200 wenzelm toplevel theorem statements support 'if'/'for' eigen-context;
Fri, 29 Apr 2016 01:21:44 +0200 wenzelm re-tuned c9605a284fba, which impacts performance significantly (for unclear reasons) -- make AFP/Collections build again;
Thu, 28 Apr 2016 11:31:36 +0200 wenzelm clarified order: params/prems/concl interchangeable with !!/==> proposition;
Thu, 28 Apr 2016 09:43:11 +0200 wenzelm support 'assumes' in specifications, e.g. 'definition', 'inductive';
Wed, 27 Apr 2016 10:03:35 +0200 wenzelm tuned;
Mon, 25 Apr 2016 16:54:48 +0200 wenzelm clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
Sun, 24 Apr 2016 20:37:24 +0200 wenzelm within a proof body context, undeclared frees are like global constants;
Mon, 18 Apr 2016 20:24:19 +0200 wenzelm prefer internal attribute source;
Fri, 15 Apr 2016 15:08:43 +0200 wenzelm clarified PIDE reports;
Wed, 30 Mar 2016 21:34:00 +0200 wenzelm tuned;
Mon, 28 Dec 2015 16:30:24 +0100 wenzelm suppress irrelevant position reports;
Mon, 28 Dec 2015 15:11:03 +0100 wenzelm more position information;
Sun, 14 Jun 2015 23:22:08 +0200 wenzelm improved treatment of Element.Obtains via Expression.prepare_stmt;
Sun, 14 Jun 2015 15:53:13 +0200 wenzelm tuned signature;
Sat, 13 Jun 2015 16:35:27 +0200 wenzelm eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
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 11:09:05 +0200 wenzelm tuned -- eliminated unused feature;
Thu, 11 Jun 2015 10:44:04 +0200 wenzelm tuned signature;
Tue, 09 Jun 2015 16:42:17 +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;
Wed, 08 Apr 2015 19:39:08 +0200 wenzelm proper context for Object_Logic operations;
Sun, 29 Mar 2015 21:30:28 +0200 wenzelm support for minimal specifications, with usual treatment of fixes and dummies;
Wed, 12 Nov 2014 18:18:38 +0100 wenzelm prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;
Fri, 31 Oct 2014 17:08:54 +0100 wenzelm eliminated odd flags and hook;
Thu, 21 Aug 2014 22:48:39 +0200 wenzelm tuned signature -- define some elementary operations earlier;
Tue, 19 Aug 2014 23:17:51 +0200 wenzelm tuned signature -- moved type src to Token, without aliases;
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;
Mon, 17 Mar 2014 10:11:23 +0100 wenzelm reject internal names, notably from Term.free_dummy_patterns;
Mon, 10 Mar 2014 15:04:01 +0100 wenzelm tuned signature -- prefer Name_Space.get with its builtin error;
Sun, 09 Mar 2014 16:37:56 +0100 wenzelm tuned signature;
Sat, 08 Mar 2014 21:08:10 +0100 wenzelm modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
Thu, 06 Mar 2014 14:38:54 +0100 wenzelm eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
Thu, 06 Mar 2014 13:44:01 +0100 wenzelm more uniform check_const/read_const;
Thu, 06 Mar 2014 12:43:29 +0100 wenzelm more rigid type_name demands, based on educated guesses about the tools involved here;
Thu, 06 Mar 2014 12:10:19 +0100 wenzelm tuned signature -- more uniform check_type_name/read_type_name;
less more (0) -100 -60 tip