| 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
|
| 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;
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 17:19:27 +0200 |
haftmann |
remove reinit operation alltogether
|
file |
diff |
annotate
|
| Tue, 10 Aug 2010 14:11:28 +0200 |
haftmann |
try to uniformly follow define/note/abbrev/declaration order as close as possible
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 11:41:27 +0200 |
wenzelm |
localized default sort;
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 19:20:52 +0200 |
wenzelm |
implicit checkpoint in Local_Theory.theory as well -- no longer export Local_Theory.checkpoint;
|
file |
diff |
annotate
|
| Mon, 15 Mar 2010 18:59:16 +0100 |
wenzelm |
replaced type_syntax/term_syntax by uniform syntax_declaration;
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 14:40:36 +0100 |
wenzelm |
added Local_Theory.alias operations (independent of target);
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 17:07:36 +0100 |
wenzelm |
more uniform treatment of syntax for types vs. consts;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 17 Nov 2009 14:50:55 +0100 |
wenzelm |
uniform new_group/reset_group;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 20:41:29 +0100 |
wenzelm |
eliminated slightly odd kind argument of LocalTheory.note(s);
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 22:06:46 +0100 |
wenzelm |
allow "pervasive" local theory declarations, which are applied the background theory;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:30:40 +0100 |
wenzelm |
modernized structure Context_Position;
|
file |
diff |
annotate
|
| 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
|
| Fri, 07 Sep 2007 20:40:08 +0200 |
wenzelm |
fixed type alias in signature;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2007 22:01:06 +0200 |
wenzelm |
type Morphism.declaration;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2007 20:40:24 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Sun, 04 Feb 2007 22:02:20 +0100 |
wenzelm |
added full_naming;
|
file |
diff |
annotate
|
| Sun, 28 Jan 2007 23:29:17 +0100 |
wenzelm |
added interface for target_naming;
|
file |
diff |
annotate
|
| Fri, 15 Dec 2006 00:08:15 +0100 |
wenzelm |
renamed LocalTheory.assert to affirm;
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 20:49:29 +0100 |
wenzelm |
abbrev: tuned signature;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 15:30:42 +0100 |
wenzelm |
added notation/abbrev (from term_syntax.ML);
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 17:58:50 +0100 |
wenzelm |
moved notation/abbrevs to TermSyntax;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2006 21:19:02 +0100 |
wenzelm |
abbrevs: actually observe target_morphism;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 22:14:49 +0100 |
wenzelm |
notation/abbreviation: more serious handling of morphisms;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 17:42:21 +0100 |
wenzelm |
added full_name;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2006 18:07:24 +0100 |
wenzelm |
abbrevs: no result;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 20:33:37 +0100 |
wenzelm |
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 18:07:29 +0100 |
wenzelm |
LocalTheory.axioms/notes/defs: proper kind;
|
file |
diff |
annotate
|
| Fri, 10 Nov 2006 22:18:52 +0100 |
wenzelm |
simplified exit;
|
file |
diff |
annotate
|
| Thu, 09 Nov 2006 21:44:31 +0100 |
wenzelm |
abbrevs: return result;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:46:48 +0100 |
wenzelm |
replaced const_syntax by notation, which operates on terms;
|
file |
diff |
annotate
|
| Sat, 14 Oct 2006 23:25:53 +0200 |
wenzelm |
added assert;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 22:55:18 +0200 |
wenzelm |
exit: pass interactive flag, toplevel result convention;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 00:27:34 +0200 |
wenzelm |
added raw_theory(_result);
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 02:20:04 +0200 |
wenzelm |
added exit;
|
file |
diff |
annotate
|
| Sat, 07 Oct 2006 01:31:16 +0200 |
wenzelm |
turned into abstract wrapper module, cf. theory_target.ML;
|
file |
diff |
annotate
|
| Fri, 29 Sep 2006 22:47:01 +0200 |
wenzelm |
Syntax.mode;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 23:42:59 +0200 |
wenzelm |
Sign.add_consts_authentic;
|
file |
diff |
annotate
|
| Sat, 29 Jul 2006 00:51:34 +0200 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 23:28:28 +0200 |
wenzelm |
renamed ProofContext.fix_frees to Variable.fix_frees;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:44:03 +0200 |
wenzelm |
"moved basic assumption operations from structure ProofContext to Assumption;"
|
file |
diff |
annotate
|
| Thu, 06 Jul 2006 23:36:40 +0200 |
wenzelm |
removed obsolete locale view;
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 15:45:59 +0200 |
ballarin |
Locales no longer generate views. The following functions have changed
|
file |
diff |
annotate
|
| Sat, 17 Jun 2006 19:37:54 +0200 |
wenzelm |
standard: simultaneous facts;
|
file |
diff |
annotate
|
| Wed, 17 May 2006 22:34:50 +0200 |
wenzelm |
export generic term_syntax;
|
file |
diff |
annotate
|
| Tue, 16 May 2006 21:33:14 +0200 |
wenzelm |
added syntax interface;
|
file |
diff |
annotate
|
| Sat, 13 May 2006 02:51:42 +0200 |
wenzelm |
Theory.add_defs(_i): added unchecked flag;
|
file |
diff |
annotate
|
| Sun, 30 Apr 2006 22:50:11 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:26 +0200 |
wenzelm |
abbrevs: support print mode;
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 18:26:01 +0100 |
wenzelm |
added abbrev element;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:35:09 +0100 |
wenzelm |
init/exit no longer change the theory (no naming);
|
file |
diff |
annotate
|
| Sun, 12 Feb 2006 21:34:26 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 11 Feb 2006 17:17:52 +0100 |
wenzelm |
added restore;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:59:51 +0100 |
wenzelm |
type local_theory = Proof.context;
|
file |
diff |
annotate
|
| Tue, 31 Jan 2006 18:19:31 +0100 |
wenzelm |
added consts_retricted;
|
file |
diff |
annotate
|
| Sat, 28 Jan 2006 17:28:57 +0100 |
wenzelm |
added print_consts;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 19:03:11 +0100 |
wenzelm |
improved 'notes', including proper treatment of locale results;
|
file |
diff |
annotate
|
| Wed, 25 Jan 2006 00:21:39 +0100 |
wenzelm |
added constant definition;
|
file |
diff |
annotate
|
| Tue, 24 Jan 2006 00:43:29 +0100 |
wenzelm |
added actual operations;
|
file |
diff |
annotate
|
| Sun, 22 Jan 2006 18:46:01 +0100 |
wenzelm |
Local theory operations, with optional target locale.
|
file |
diff |
annotate
|