Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/named_target.ML
Wed, 26 Feb 2014 10:53:19 +0100 wenzelm tuned signature; file | diff | annotate
Mon, 19 Aug 2013 20:47:09 +0200 wenzelm tuned; file | diff | annotate
Sat, 25 May 2013 15:44:08 +0200 haftmann tuned structure file | diff | annotate
Tue, 21 May 2013 17:45:53 +0200 wenzelm more markup; file | diff | annotate
Mon, 18 Jun 2012 15:48:43 +0200 haftmann class target handles additional non-class term parameters appropriately file | diff | annotate
Tue, 03 Apr 2012 13:47:15 +0200 wenzelm tuned; file | diff | annotate
Tue, 03 Apr 2012 11:28:21 +0200 wenzelm clarified generic_const vs. close_schematic_term; file | diff | annotate
Tue, 03 Apr 2012 10:59:20 +0200 wenzelm more uniform theory_abbrev with const_declaration; file | diff | annotate
Tue, 03 Apr 2012 09:47:20 +0200 wenzelm clarified background_foundation vs. theory_foundation (with const_declaration); file | diff | annotate
Tue, 03 Apr 2012 09:41:16 +0200 wenzelm tuned; file | diff | annotate
Mon, 02 Apr 2012 23:55:25 +0200 wenzelm more general standard_declaration; file | diff | annotate
Mon, 02 Apr 2012 21:49:27 +0200 wenzelm clarified standard_declaration vs. theory_declaration; file | diff | annotate
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); file | diff | annotate
Mon, 02 Apr 2012 20:12:17 +0200 wenzelm tuned; file | diff | annotate
Mon, 02 Apr 2012 19:47:21 +0200 wenzelm tuned signature; file | diff | annotate
Mon, 02 Apr 2012 19:10:52 +0200 wenzelm misc tuning and simplification; file | diff | annotate
Sun, 01 Apr 2012 20:42:19 +0200 wenzelm nothing specific about named target; file | diff | annotate
Sun, 01 Apr 2012 20:36:33 +0200 wenzelm clarified Generic_Target.notes: always perform Attrib.partial_evaluation; file | diff | annotate
Sun, 01 Apr 2012 18:01:19 +0200 wenzelm tuned signature; file | diff | annotate
Sun, 01 Apr 2012 15:23:43 +0200 wenzelm clarified Named_Target.target_declaration: propagate through other levels as well; file | diff | annotate
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); file | diff | annotate
Thu, 22 Mar 2012 11:11:51 +0100 wenzelm tuned; file | diff | annotate
Wed, 21 Mar 2012 23:26:35 +0100 wenzelm more explicit Toplevel.open_target/close_target; file | diff | annotate
Wed, 21 Mar 2012 17:25:35 +0100 wenzelm basic support for nested contexts including bundles; file | diff | annotate
Wed, 21 Mar 2012 11:25:19 +0100 wenzelm clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2); file | diff | annotate
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; file | diff | annotate
Sun, 20 Nov 2011 17:57:09 +0100 wenzelm tuned signature; file | diff | annotate
Fri, 18 Nov 2011 21:55:24 +0100 wenzelm partial evaluation of locale facts leads to static scoping of rule attributes; file | diff | annotate
Mon, 14 Nov 2011 16:52:19 +0100 wenzelm pass positions for named targets, for formal links in the document model; file | diff | annotate
Mon, 07 Nov 2011 17:00:23 +0100 wenzelm tuned signature -- avoid spurious Thm.mixed_attribute; file | diff | annotate
Sun, 06 Nov 2011 21:51:46 +0100 wenzelm more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; file | diff | annotate
Sat, 05 Nov 2011 22:41:25 +0100 wenzelm tuned; file | diff | annotate
Sat, 05 Nov 2011 22:01:19 +0100 wenzelm misc tuning; file | diff | annotate
Sun, 30 Oct 2011 22:35:18 +0100 wenzelm even more uniform Local_Theory.declaration for locales (cf. 57def0b39696, aa35859c8741); file | diff | annotate
Sun, 30 Oct 2011 22:20:45 +0100 wenzelm removed obsolete argument (cf. aa35859c8741); file | diff | annotate
Sat, 29 Oct 2011 12:57:43 +0200 wenzelm uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally); file | diff | annotate
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; file | diff | annotate
Fri, 28 Oct 2011 22:17:30 +0200 wenzelm uniform Local_Theory.declaration with explicit params; file | diff | annotate
Fri, 28 Oct 2011 17:15:52 +0200 wenzelm tuned signature -- refined terminology; file | diff | annotate
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context; file | diff | annotate
Sun, 13 Mar 2011 22:55:50 +0100 wenzelm tuned headers; file | diff | annotate
Sun, 16 Jan 2011 14:57:14 +0100 wenzelm added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management; file | diff | annotate
Sun, 28 Nov 2010 15:28:48 +0100 wenzelm superficial tuning; file | diff | annotate
Wed, 22 Sep 2010 12:22:47 +0200 haftmann tuned file | diff | annotate
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only; file | diff | annotate
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; file | diff | annotate
Fri, 20 Aug 2010 08:52:01 +0200 haftmann tuned: less formal noise in Named_Target, more coherence in Class file | diff | annotate
Thu, 12 Aug 2010 13:53:42 +0200 haftmann Class.declare -> Class.const file | diff | annotate
Thu, 12 Aug 2010 13:42:13 +0200 haftmann named target is optional; explicit Name_Target.reinit file | diff | annotate
Thu, 12 Aug 2010 13:28:18 +0200 haftmann Named_Target.init: empty string represents theory target file | diff | annotate
Thu, 12 Aug 2010 13:23:46 +0200 haftmann Named_Target.theory_init file | diff | annotate
Wed, 11 Aug 2010 17:19:27 +0200 haftmann remove reinit operation alltogether file | diff | annotate
Wed, 11 Aug 2010 16:02:03 +0200 haftmann more convenient split of class modules: class and class_declaration file | diff | annotate
Wed, 11 Aug 2010 15:45:15 +0200 haftmann tuned file | diff | annotate
Wed, 11 Aug 2010 14:45:38 +0200 haftmann renamed Theory_Target to the more appropriate Named_Target file | diff | annotate | base
less more (0) tip
isabelle