src/Pure/Isar/named_target.ML
Mon, 13 Oct 2014 21:41:29 +0200 wenzelm tuned signature;
Wed, 02 Jul 2014 08:03:50 +0200 haftmann optional exit hook for theory-like targets
Wed, 02 Jul 2014 08:03:49 +0200 haftmann restore exactly named target, prevent non-named targets to participate in the ad-hoc switch game
Wed, 02 Jul 2014 08:03:48 +0200 haftmann centralized (ad-hoc) switching of targets in named_target.ML
Sun, 08 Jun 2014 23:30:53 +0200 haftmann tuned data structure
Sun, 08 Jun 2014 23:30:52 +0200 haftmann recovered level-free fishing for locale, accidentally lost in dce365931721
Sun, 08 Jun 2014 23:30:51 +0200 haftmann self-contained locale_declaration operation
Sun, 08 Jun 2014 23:30:51 +0200 haftmann yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
Sat, 07 Jun 2014 08:16:03 +0200 haftmann tuned
Sat, 07 Jun 2014 08:16:03 +0200 haftmann avoid odd Named_Target.reinit altogether
Sat, 07 Jun 2014 08:16:03 +0200 haftmann less baroque interface
Fri, 06 Jun 2014 19:19:46 +0200 haftmann dropped obscure and unused ad-hoc before_exit hook for named targets
Thu, 05 Jun 2014 19:39:38 +0200 haftmann sharpened criterion: bare named target is only at the bottom level
Thu, 05 Jun 2014 19:39:35 +0200 haftmann tuned
Mon, 02 Jun 2014 19:21:41 +0200 haftmann formal treatment of dangling parameters for class abbrevs analogously to class consts
Mon, 02 Jun 2014 19:21:40 +0200 haftmann explicit passing of params
Fri, 30 May 2014 08:23:07 +0200 haftmann tuned signature
Thu, 29 May 2014 22:46:21 +0200 haftmann more direct passing of right-hand side
Wed, 28 May 2014 19:17:32 +0200 haftmann tuned variable names
Thu, 22 May 2014 17:53:02 +0200 haftmann tuned names
Thu, 22 May 2014 17:53:01 +0200 haftmann tuned signature
Thu, 22 May 2014 17:53:01 +0200 haftmann moved const declaration further down in bootstrap hierarchy: keep Named_Target free of low-level stuff
Thu, 22 May 2014 17:52:59 +0200 haftmann unused
Thu, 22 May 2014 16:59:49 +0200 haftmann common background_abbrev operation
Thu, 22 May 2014 16:59:49 +0200 haftmann tuned signature
Thu, 22 May 2014 16:59:49 +0200 haftmann tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction
Thu, 22 May 2014 16:59:49 +0200 haftmann compactified
Thu, 22 May 2014 09:40:05 +0200 haftmann compactified level discriminator
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, 19 Aug 2013 20:47:09 +0200 wenzelm tuned;
Sat, 25 May 2013 15:44:08 +0200 haftmann tuned structure
Tue, 21 May 2013 17:45:53 +0200 wenzelm more markup;
Mon, 18 Jun 2012 15:48:43 +0200 haftmann class target handles additional non-class term parameters appropriately
Tue, 03 Apr 2012 13:47:15 +0200 wenzelm tuned;
Tue, 03 Apr 2012 11:28:21 +0200 wenzelm clarified generic_const vs. close_schematic_term;
Tue, 03 Apr 2012 10:59:20 +0200 wenzelm more uniform theory_abbrev with const_declaration;
Tue, 03 Apr 2012 09:47:20 +0200 wenzelm clarified background_foundation vs. theory_foundation (with const_declaration);
Tue, 03 Apr 2012 09:41:16 +0200 wenzelm tuned;
Mon, 02 Apr 2012 23:55:25 +0200 wenzelm more general standard_declaration;
Mon, 02 Apr 2012 21:49:27 +0200 wenzelm clarified standard_declaration vs. theory_declaration;
Mon, 02 Apr 2012 20:50:41 +0200 wenzelm smarter generic_const: plain alias for non-dependent case (e.g. prospective datatype or record syntax);
Mon, 02 Apr 2012 20:12:17 +0200 wenzelm tuned;
Mon, 02 Apr 2012 19:47:21 +0200 wenzelm tuned signature;
Mon, 02 Apr 2012 19:10:52 +0200 wenzelm misc tuning and simplification;
Sun, 01 Apr 2012 20:42:19 +0200 wenzelm nothing specific about named target;
Sun, 01 Apr 2012 20:36:33 +0200 wenzelm clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
Sun, 01 Apr 2012 18:01:19 +0200 wenzelm tuned signature;
Sun, 01 Apr 2012 15:23:43 +0200 wenzelm clarified Named_Target.target_declaration: propagate through other levels as well;
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 11:11:51 +0100 wenzelm tuned;
Wed, 21 Mar 2012 23:26:35 +0100 wenzelm more explicit Toplevel.open_target/close_target;
Wed, 21 Mar 2012 17:25:35 +0100 wenzelm basic support for nested contexts including bundles;
Wed, 21 Mar 2012 11:25:19 +0100 wenzelm clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
Sat, 17 Mar 2012 23:50:47 +0100 wenzelm amended locale_declaration: avoid duplication of Local_Theory.target with global_morphism (cf. 57def0b39696) -- Haftmann-Wenzel Sandwich has 3 layers, not 4;
Sun, 20 Nov 2011 17:57:09 +0100 wenzelm tuned signature;
Fri, 18 Nov 2011 21:55:24 +0100 wenzelm partial evaluation of locale facts leads to static scoping of rule attributes;
Mon, 14 Nov 2011 16:52:19 +0100 wenzelm pass positions for named targets, for formal links in the document model;
Mon, 07 Nov 2011 17:00:23 +0100 wenzelm tuned signature -- avoid spurious Thm.mixed_attribute;
less more (0) -60 tip