| 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
|