src/Pure/Isar/overloading.ML
Fri, 25 Apr 2014 21:45:04 +0200 haftmann subscription as target-specific implementation device
Tue, 11 Mar 2014 22:49:28 +0100 wenzelm more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
Wed, 26 Feb 2014 10:53:19 +0100 wenzelm tuned signature;
Mon, 03 Feb 2014 16:33:54 +0100 wenzelm more formal markup;
Tue, 30 Jul 2013 15:09:25 +0200 wenzelm type theory is purely value-oriented;
Tue, 03 Apr 2012 13:47:15 +0200 wenzelm tuned;
Tue, 03 Apr 2012 10:59:20 +0200 wenzelm more uniform theory_abbrev with const_declaration;
Mon, 02 Apr 2012 21:49:27 +0200 wenzelm clarified standard_declaration vs. theory_declaration;
Sun, 01 Apr 2012 20:36:33 +0200 wenzelm clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
Sun, 01 Apr 2012 14:29:22 +0200 wenzelm Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom;
Thu, 22 Mar 2012 15:41:49 +0100 wenzelm uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
Thu, 22 Mar 2012 10:49:31 +0100 wenzelm synchronize syntax uniformly for target stack and aux. context;
Wed, 21 Mar 2012 11:25:19 +0100 wenzelm clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
Wed, 14 Mar 2012 18:09:05 +0100 wenzelm tuned messages;
Wed, 14 Mar 2012 11:45:16 +0100 wenzelm Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
Thu, 10 Nov 2011 17:47:25 +0100 wenzelm tuned signature;
Wed, 09 Nov 2011 20:47:11 +0100 wenzelm tuned signature;
Sun, 30 Oct 2011 22:20:45 +0100 wenzelm removed obsolete argument (cf. aa35859c8741);
Fri, 28 Oct 2011 23:16:50 +0200 wenzelm refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
Fri, 28 Oct 2011 22:17:30 +0200 wenzelm uniform Local_Theory.declaration with explicit params;
Tue, 19 Apr 2011 16:13:04 +0200 wenzelm minor tuning and modernization;
Tue, 19 Apr 2011 14:57:09 +0200 wenzelm simplified check/uncheck interfaces: result comparison is hardwired by default;
Mon, 18 Apr 2011 13:52:23 +0200 wenzelm standardized aliases of operations on tsig;
Sun, 17 Apr 2011 19:54:04 +0200 wenzelm report Name_Space.declare/define, relatively to context;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Sat, 16 Apr 2011 15:25:25 +0200 wenzelm prefer local name spaces;
Sun, 28 Nov 2010 15:28:48 +0100 wenzelm superficial tuning;
Mon, 13 Sep 2010 16:15:12 +0200 haftmann more precise name for activation of improveable syntax
Thu, 26 Aug 2010 15:48:08 +0200 wenzelm renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
Wed, 11 Aug 2010 17:59:32 +0200 haftmann tuned internal structure
Wed, 11 Aug 2010 17:19:27 +0200 haftmann remove reinit operation alltogether
Wed, 11 Aug 2010 15:09:31 +0200 haftmann stripped signature
Wed, 11 Aug 2010 12:30:48 +0200 haftmann moved overloading target formally to overloading.ML
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;
Mon, 26 Apr 2010 20:30:50 +0200 wenzelm eliminanated some unreferenced identifiers;
Sun, 11 Apr 2010 14:30:34 +0200 wenzelm Thm.add_axiom/add_def: return internal name of foundational axiom;
Sun, 21 Mar 2010 08:46:50 +0100 haftmann tuned whitespace
Mon, 15 Feb 2010 14:04:06 +0100 haftmann clarifed type
Fri, 13 Nov 2009 21:11:15 +0100 wenzelm modernized structure Local_Theory;
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Sat, 15 Aug 2009 15:29:54 +0200 haftmann additional checkpoints avoid problems in error situations
Thu, 30 Jul 2009 15:21:18 +0200 haftmann improved handling of parameters
Fri, 17 Jul 2009 23:11:40 +0200 wenzelm tuned/modernized Envir.subst_XXX;
Wed, 17 Jun 2009 17:42:46 +0200 haftmann uncheck is liberal wrt. semityped terms
Fri, 13 Mar 2009 19:17:58 +0100 haftmann coherent binding policy with primitive target operations
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Wed, 21 Jan 2009 16:47:04 +0100 haftmann binding replaces bstring
Thu, 19 Jun 2008 22:05:04 +0200 wenzelm ProofContext.abbrev_mode;
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Tue, 22 Apr 2008 08:33:12 +0200 haftmann proper abbreviations in class
Thu, 10 Apr 2008 00:46:40 +0200 haftmann improvements are strict
Wed, 02 Apr 2008 15:58:43 +0200 haftmann tuned
Wed, 12 Mar 2008 08:47:35 +0100 haftmann better improvement in instantiation target
Mon, 10 Mar 2008 21:51:47 +0100 haftmann tuned
Fri, 07 Mar 2008 13:53:07 +0100 haftmann generic improvable syntax for targets
Tue, 08 Jan 2008 11:37:27 +0100 haftmann refined overloading target
Tue, 11 Dec 2007 10:23:13 +0100 haftmann continued
Wed, 05 Dec 2007 14:15:51 +0100 haftmann improved
Mon, 03 Dec 2007 16:04:17 +0100 haftmann overloading target
less more (0) tip