| Wed, 28 Oct 2009 17:36:34 +0100 |
wenzelm |
let naming transform binding beforehand -- covering only the "conceal" flag for now;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 16:25:10 +0100 |
wenzelm |
added restore_naming;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 19:18:25 +0100 |
wenzelm |
maintain proper Name_Space.naming, with conceal and set_group;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 12:27:21 +0100 |
wenzelm |
allow name space entries to be "concealed" -- via binding/naming/local_theory;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 19:47:37 +0200 |
wenzelm |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 11:44:34 +0100 |
wenzelm |
added map_contexts (cf. Proof.map_contexts);
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 13:18:42 +0100 |
wenzelm |
renamed sticky_prefix to mandatory_path;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:32 +0100 |
haftmann |
binding is alias for Binding.T
|
file |
diff |
annotate
|
| Wed, 17 Dec 2008 12:10:39 +0100 |
haftmann |
dropped Ids
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 08:04:53 +0100 |
haftmann |
dropped NameSpace.declare_base
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 14:41:24 +0200 |
wenzelm |
target update: invisible context position avoids duplication of reports etc.;
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 10:58:03 +0200 |
wenzelm |
added exit_global, exit_result, exit_result_global;
|
file |
diff |
annotate
|
| Sat, 27 Sep 2008 15:20:39 +0200 |
wenzelm |
Theory.checkpoint for main operations, admits concurrent proofs;
|
file |
diff |
annotate
|
| Wed, 03 Sep 2008 17:47:40 +0200 |
wenzelm |
discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 16:55:33 +0200 |
wenzelm |
type Attrib.binding abbreviates Name.binding without attributes;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:45 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 11:48:54 +0200 |
wenzelm |
type Properties.T;
|
file |
diff |
annotate
|
| Mon, 25 Feb 2008 16:31:19 +0100 |
wenzelm |
maintain group in lthy data, implicit use in operations;
|
file |
diff |
annotate
|
| Sat, 26 Jan 2008 17:08:43 +0100 |
wenzelm |
grouped versions of axioms/define/notes;
|
file |
diff |
annotate
|
| Sat, 10 Nov 2007 18:36:10 +0100 |
wenzelm |
removed LocalTheory.target_naming/name;
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 20:50:42 +0100 |
wenzelm |
simplified LocalTheory.reinit;
|
file |
diff |
annotate
|
| Sat, 20 Oct 2007 18:54:33 +0200 |
wenzelm |
tuned abbrev interface;
|
file |
diff |
annotate
|
| Fri, 19 Oct 2007 20:57:14 +0200 |
wenzelm |
tuned interfaces;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2007 00:18:07 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 13 Oct 2007 17:16:44 +0200 |
wenzelm |
renamed def to define;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 21:10:40 +0200 |
wenzelm |
local_theory: incorporated consts into axioms;
|
file |
diff |
annotate
|
| Wed, 10 Oct 2007 17:31:56 +0200 |
wenzelm |
generalized notation interface (add or del);
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 17:10:46 +0200 |
wenzelm |
removed LocalTheory.defs/target_morphism operations;
|
file |
diff |
annotate
|