src/Pure/variable.ML
Mon, 03 Jun 2019 21:47:54 +0200 wenzelm more structural integrity;
Mon, 03 Jun 2019 15:40:08 +0200 wenzelm clarified signature;
Mon, 03 Jun 2019 13:28:01 +0200 wenzelm tuned signature;
Thu, 03 Jan 2019 15:55:36 +0100 wenzelm tuned signature;
Thu, 03 Jan 2019 14:12:44 +0100 wenzelm clarified signature: more types;
Sun, 25 Feb 2018 15:44:46 +0100 wenzelm eliminated ASCII syntax from Pure bootstrap;
Tue, 13 Dec 2016 11:51:42 +0100 wenzelm more symbols;
Thu, 14 Apr 2016 23:31:10 +0200 wenzelm highlighting of entity def/ref positions wrt. cursor;
Mon, 11 Apr 2016 15:50:18 +0200 wenzelm back to dummy constraints (amending dd2914250ca7): important for Syntax_Phases.get_free/is_declared;
Wed, 30 Mar 2016 22:00:55 +0200 wenzelm more accurate mixfix type constraints;
Thu, 31 Dec 2015 15:27:25 +0100 wenzelm more precise context -- potentially relevant for Eisbach dummy thm;
Mon, 28 Dec 2015 16:29:39 +0100 wenzelm suppress irrelevant position reports;
Wed, 23 Dec 2015 20:23:44 +0100 wenzelm clarified context policy to allow multiple dummies;
Fri, 23 Oct 2015 17:17:11 +0200 wenzelm clarified modules;
Tue, 28 Jul 2015 21:10:41 +0200 wenzelm clarified Variable.gen_all;
Tue, 28 Jul 2015 20:59:39 +0200 wenzelm more explicit context;
Mon, 27 Jul 2015 23:40:39 +0200 wenzelm tuned signature;
Thu, 09 Jul 2015 22:36:31 +0200 wenzelm SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
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);
Tue, 09 Jun 2015 11:51:05 +0200 wenzelm clarified term bindings;
Wed, 03 Jun 2015 19:25:05 +0200 wenzelm clarified context;
Tue, 31 Mar 2015 20:18:10 +0200 wenzelm tuned signature;
Tue, 31 Mar 2015 20:07:37 +0200 wenzelm tuned signature;
Sun, 29 Mar 2015 21:58:10 +0200 wenzelm tuned signature;
Sat, 28 Mar 2015 17:26:42 +0100 wenzelm prefer Variable.focus, despite subtle differences of Logic.strip_params vs. Term.strip_all_vars;
Tue, 24 Mar 2015 16:17:07 +0100 wenzelm tuned;
Tue, 24 Mar 2015 15:57:51 +0100 wenzelm admit dummy patterns in instantiations;
Mon, 23 Mar 2015 22:57:04 +0100 wenzelm implicit goal parameters are improper;
Sat, 07 Mar 2015 15:40:36 +0100 wenzelm added declare_maxidx operations for Eisbach;
Sat, 07 Mar 2015 12:32:55 +0100 wenzelm clarified Variable.export: observe maxidx of target context;
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, 21 Dec 2014 22:49:17 +0100 wenzelm tuned signature;
Fri, 19 Dec 2014 12:36:50 +0100 wenzelm tuned;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Mon, 13 Oct 2014 22:43:29 +0200 wenzelm tuned signature;
Mon, 10 Mar 2014 13:55:03 +0100 wenzelm abstract type Name_Space.table;
Thu, 06 Mar 2014 10:12:47 +0100 wenzelm tuned signature;
Thu, 20 Feb 2014 21:27:14 +0100 wenzelm tuned signature;
Wed, 15 Jan 2014 22:24:57 +0100 wenzelm general notion of auxiliary bounds within context;
Fri, 13 Dec 2013 20:20:15 +0100 wenzelm maintain morphism names for diagnostic purposes;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Wed, 03 Oct 2012 16:43:41 +0200 wenzelm tuned;
Wed, 03 Oct 2012 14:58:56 +0200 wenzelm allow position constraints to coexist with 0 or 1 sort constraints;
Mon, 01 Oct 2012 16:37:22 +0200 wenzelm report sort assignment of visible type variables;
Mon, 19 Mar 2012 20:32:57 +0100 wenzelm clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
Sun, 11 Mar 2012 14:09:01 +0100 wenzelm more direct Name_Space.defined_entry;
Wed, 15 Feb 2012 23:19:30 +0100 wenzelm renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Sun, 27 Nov 2011 21:53:38 +0100 wenzelm tuned;
Sat, 12 Nov 2011 18:05:31 +0100 wenzelm tuned markup -- prefer user-perspective;
Fri, 11 Nov 2011 14:07:20 +0100 wenzelm discontinued entity text color, notably historic red for classes;
Wed, 09 Nov 2011 17:12:26 +0100 wenzelm tuned;
Mon, 07 Nov 2011 23:03:52 +0100 wenzelm tuned;
Fri, 28 Oct 2011 15:38:41 +0200 wenzelm slightly more explicit/syntactic modelling of morphisms;
Tue, 12 Jul 2011 23:22:22 +0200 wenzelm more thorough Variable.check_name: Binding.check for logical entities within the term language;
Thu, 09 Jun 2011 20:22:22 +0200 wenzelm tuned signature: Name.invent and Name.invent_names;
less more (0) -100 -60 tip