src/Pure/Isar/local_theory.ML
Sat, 01 Sep 2012 19:43:18 +0200 wenzelm discontinued complicated/unreliable notion of recent proofs within context;
Fri, 31 Aug 2012 22:24:14 +0200 wenzelm tuned signature;
Fri, 31 Aug 2012 16:35:30 +0200 wenzelm more precise register_proofs for local goals;
Mon, 02 Apr 2012 23:27:24 +0200 wenzelm better restore after close_target;
Mon, 02 Apr 2012 17:00:32 +0200 wenzelm better restore to first target, not last target;
Mon, 02 Apr 2012 15:42:50 +0200 wenzelm more general Local_Theory.restore, allow any nesting level;
Sun, 01 Apr 2012 18:01:19 +0200 wenzelm tuned signature;
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);
Wed, 21 Mar 2012 17:25:35 +0100 wenzelm basic support for nested contexts including bundles;
Wed, 21 Mar 2012 15:19:45 +0100 wenzelm basic support for nested local theory targets;
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 16:07:03 +0100 wenzelm refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
Sat, 29 Oct 2011 12:57:43 +0200 wenzelm uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
Fri, 28 Oct 2011 22:17:30 +0200 wenzelm uniform Local_Theory.declaration with explicit params;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
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;
Thu, 26 Aug 2010 13:09:12 +0200 wenzelm renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
Wed, 11 Aug 2010 17:19:27 +0200 haftmann remove reinit operation alltogether
Tue, 10 Aug 2010 14:11:28 +0200 haftmann try to uniformly follow define/note/abbrev/declaration order as close as possible
Sat, 24 Jul 2010 12:14:53 +0200 wenzelm moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
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;
Wed, 28 Apr 2010 11:41:27 +0200 wenzelm localized default sort;
Sun, 28 Mar 2010 19:20:52 +0200 wenzelm implicit checkpoint in Local_Theory.theory as well -- no longer export Local_Theory.checkpoint;
Mon, 15 Mar 2010 18:59:16 +0100 wenzelm replaced type_syntax/term_syntax by uniform syntax_declaration;
Sat, 13 Mar 2010 14:40:36 +0100 wenzelm added Local_Theory.alias operations (independent of target);
Mon, 01 Mar 2010 17:07:36 +0100 wenzelm more uniform treatment of syntax for types vs. consts;
Thu, 19 Nov 2009 14:44:22 +0100 wenzelm Local_Theory.define: eliminated slightly odd kind argument -- such low-level definitions should be hardly ever exposed to end-users anyway;
Tue, 17 Nov 2009 14:50:55 +0100 wenzelm uniform new_group/reset_group;
Fri, 13 Nov 2009 21:11:15 +0100 wenzelm modernized structure Local_Theory;
Fri, 13 Nov 2009 20:41:29 +0100 wenzelm eliminated slightly odd kind argument of LocalTheory.note(s);
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Thu, 05 Nov 2009 22:06:46 +0100 wenzelm allow "pervasive" local theory declarations, which are applied the background theory;
Mon, 02 Nov 2009 20:30:40 +0100 wenzelm modernized structure Context_Position;
Wed, 28 Oct 2009 17:36:34 +0100 wenzelm let naming transform binding beforehand -- covering only the "conceal" flag for now;
Wed, 28 Oct 2009 16:25:10 +0100 wenzelm added restore_naming;
Sun, 25 Oct 2009 19:18:25 +0100 wenzelm maintain proper Name_Space.naming, with conceal and set_group;
Sun, 25 Oct 2009 12:27:21 +0100 wenzelm allow name space entries to be "concealed" -- via binding/naming/local_theory;
Sat, 24 Oct 2009 19:47:37 +0200 wenzelm renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
Thu, 19 Mar 2009 11:44:34 +0100 wenzelm added map_contexts (cf. Proof.map_contexts);
Thu, 12 Mar 2009 13:18:42 +0100 wenzelm renamed sticky_prefix to mandatory_path;
Wed, 11 Mar 2009 16:36:27 +0100 wenzelm eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
Wed, 21 Jan 2009 16:47:32 +0100 haftmann binding is alias for Binding.T
Wed, 17 Dec 2008 12:10:39 +0100 haftmann dropped Ids
Fri, 05 Dec 2008 08:04:53 +0100 haftmann dropped NameSpace.declare_base
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Mon, 29 Sep 2008 14:41:24 +0200 wenzelm target update: invisible context position avoids duplication of reports etc.;
Mon, 29 Sep 2008 10:58:03 +0200 wenzelm added exit_global, exit_result, exit_result_global;
Sat, 27 Sep 2008 15:20:39 +0200 wenzelm Theory.checkpoint for main operations, admits concurrent proofs;
Wed, 03 Sep 2008 17:47:40 +0200 wenzelm discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
Tue, 02 Sep 2008 16:55:33 +0200 wenzelm type Attrib.binding abbreviates Name.binding without attributes;
Tue, 02 Sep 2008 14:10:45 +0200 wenzelm explicit type Name.binding for higher-specification elements;
Wed, 27 Aug 2008 11:48:54 +0200 wenzelm type Properties.T;
Mon, 25 Feb 2008 16:31:19 +0100 wenzelm maintain group in lthy data, implicit use in operations;
Sat, 26 Jan 2008 17:08:43 +0100 wenzelm grouped versions of axioms/define/notes;
Sat, 10 Nov 2007 18:36:10 +0100 wenzelm removed LocalTheory.target_naming/name;
Mon, 05 Nov 2007 20:50:42 +0100 wenzelm simplified LocalTheory.reinit;
Sat, 20 Oct 2007 18:54:33 +0200 wenzelm tuned abbrev interface;
Fri, 19 Oct 2007 20:57:14 +0200 wenzelm tuned interfaces;
Sun, 14 Oct 2007 00:18:07 +0200 wenzelm tuned;
less more (0) -100 -60 tip