src/Pure/variable.ML
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;
Thu, 09 Jun 2011 17:51:49 +0200 wenzelm simplified Name.variant -- discontinued builtin fold_map;
Wed, 27 Apr 2011 21:50:04 +0200 wenzelm clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
Wed, 27 Apr 2011 20:58:40 +0200 wenzelm tuned signature -- eliminated odd comment;
Wed, 27 Apr 2011 20:37:56 +0200 wenzelm more informative markup for fixed variables (via name space entry);
Wed, 27 Apr 2011 17:58:45 +0200 wenzelm reorganized fixes as specialized (global) name space;
Wed, 27 Apr 2011 10:31:18 +0200 wenzelm more uniform Variable.add_frees/add_fixed etc.;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Sat, 16 Apr 2011 12:46:18 +0200 wenzelm tuned signature, disentangled dependencies;
Mon, 25 Oct 2010 11:22:30 +0200 wenzelm recovered some odd two-dimensional layout;
Fri, 24 Sep 2010 15:53:13 +0200 wenzelm modernized structure Ord_List;
Sun, 12 Sep 2010 20:47:47 +0200 wenzelm load type_infer.ML later -- proper context for Type_Infer.infer_types;
Fri, 27 Aug 2010 19:43:28 +0200 wenzelm more careful treatment of context visibility flag wrt. spurious warnings;
Thu, 27 May 2010 17:41:27 +0200 wenzelm renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
Tue, 04 May 2010 12:30:15 +0200 wenzelm simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Fri, 30 Apr 2010 23:53:37 +0200 wenzelm renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
Wed, 25 Nov 2009 09:13:46 +0100 haftmann normalized uncurry take/drop
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Wed, 21 Oct 2009 12:09:37 +0200 haftmann curried inter as canonical list operation (beware of argument order)
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
Wed, 30 Sep 2009 22:20:58 +0200 wenzelm eliminated redundant bindings;
Thu, 30 Jul 2009 01:14:40 +0200 wenzelm Variable.importT/import: return full instantiations, tuned;
Sun, 26 Jul 2009 13:12:54 +0200 wenzelm Variable.focus: named parameters;
Thu, 09 Jul 2009 22:48:12 +0200 wenzelm renamed structure TermSubst to Term_Subst;
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);
Sat, 28 Mar 2009 16:30:09 +0100 wenzelm replaced add_binds by singleton bind_term;
Wed, 21 Jan 2009 22:26:49 +0100 wenzelm eliminated obsolete var morphism;
Wed, 31 Dec 2008 19:54:04 +0100 wenzelm Term.declare_typ_names, Term.declare_term_frees;
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Thu, 16 Oct 2008 22:44:34 +0200 wenzelm maintain sort occurrences of declared terms;
Thu, 19 Jun 2008 20:48:04 +0200 wenzelm added declare_typ;
Tue, 10 Jun 2008 16:43:21 +0200 wenzelm focus: actually declare constraints for local parameters;
Thu, 17 Apr 2008 22:22:26 +0200 wenzelm variant_fixes: preserve internal state, mark skolem only for body mode;
Fri, 07 Dec 2007 15:08:08 +0100 haftmann exported declare_names
Wed, 07 Nov 2007 16:42:57 +0100 wenzelm refined notion of consts within the local scope;
Tue, 06 Nov 2007 22:50:34 +0100 wenzelm added is_const/declare_const for local scope of fixes/consts;
Tue, 16 Oct 2007 17:06:15 +0200 wenzelm add_bind: close_schematic_term;
Thu, 04 Oct 2007 20:29:24 +0200 wenzelm replaced literal 'a by Name.aT;
Sat, 29 Sep 2007 21:39:50 +0200 wenzelm maintain maxidx (analogous to name context);
Wed, 26 Sep 2007 11:27:46 +0200 wenzelm declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
Mon, 24 Sep 2007 21:07:39 +0200 wenzelm added polymorphic_types;
Mon, 07 May 2007 00:49:59 +0200 wenzelm simplified DataFun interfaces;
Sun, 15 Apr 2007 23:25:54 +0200 wenzelm removed obsolete redeclare_skolems;
Sun, 15 Apr 2007 14:31:47 +0200 wenzelm Thm.fold_terms;
Sat, 14 Apr 2007 00:46:21 +0200 wenzelm tuned signature;
less more (0) -60 tip