| Wed, 28 Jul 2010 00:13:26 +0200 |
wenzelm |
explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents;
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 23:01:42 +0200 |
wenzelm |
theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 22:00:26 +0200 |
wenzelm |
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
|
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
|
| Wed, 21 Jul 2010 16:14:16 +0200 |
wenzelm |
eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing;
|
file |
diff |
annotate
|
| Tue, 20 Jul 2010 21:57:26 +0200 |
wenzelm |
warning in proper transaction context;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Sun, 30 May 2010 21:34:19 +0200 |
wenzelm |
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 23:40:00 +0200 |
wenzelm |
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 23:32:15 +0200 |
wenzelm |
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 23:23:45 +0200 |
wenzelm |
renamed structure ValueParse to Parse_Value;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 23:16:32 +0200 |
wenzelm |
refer directly to structure Keyword and Parse;
|
file |
diff |
annotate
|
| Wed, 12 May 2010 15:25:58 +0200 |
wenzelm |
updated/unified some legacy warnings;
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 16:55:22 +0200 |
wenzelm |
ProofContext.read_const: allow for type constraint (for fixed variable);
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 12:07:52 +0200 |
wenzelm |
renamed command 'defaultsort' to 'default_sort';
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 11:41:27 +0200 |
wenzelm |
localized default sort;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 11:09:19 +0200 |
wenzelm |
modernized/simplified Sign.set_defsort;
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 21:45:08 +0200 |
wenzelm |
command 'example_proof' opens an empty proof body;
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 15:52:03 +0200 |
wenzelm |
modernized naming conventions of main Isar proof elements;
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 22:48:07 +0200 |
wenzelm |
explicit 'schematic_theorem' etc. for schematic theorem statements;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 22:18:59 +0200 |
wenzelm |
keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 20:17:38 +0200 |
wenzelm |
modernized old-style type abbreviations;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 19:43:06 +0200 |
wenzelm |
local type abbreviations;
|
file |
diff |
annotate
|
| Sun, 11 Apr 2010 16:51:07 +0200 |
haftmann |
user interface for abstract datatypes is an attribute, not a command
|
file |
diff |
annotate
|
| Sun, 21 Mar 2010 19:28:25 +0100 |
wenzelm |
minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 22:59:44 +0100 |
wenzelm |
typedecl: no sort constraints;
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 23:32:13 +0100 |
wenzelm |
localized typedecl;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:47:02 +0100 |
wenzelm |
separate structure Typedecl;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 17:09:42 +0100 |
wenzelm |
added type_notation command;
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 20:37:01 +0100 |
wenzelm |
allow general mixfix syntax for type constructors;
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 10:11:12 +0100 |
haftmann |
dropped axclass
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 11:06:20 +0100 |
haftmann |
added code_abstype keyword
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 23:41:01 +0100 |
wenzelm |
removed unused Theory_Target.begin;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 16:04:57 +0100 |
wenzelm |
modernized structure Theory_Target;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 14:38:36 +0100 |
wenzelm |
print_theorems: suppress concealed (global) facts, unless "!" option is given;
|
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 21:03:41 +0100 |
wenzelm |
modernized structure Proof_Node;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 22:00:35 +0100 |
wenzelm |
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 07:40:25 +0200 |
ballarin |
Merged.
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 22:15:54 +0200 |
ballarin |
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
|
file |
diff |
annotate
|
| Tue, 01 Sep 2009 14:45:06 +0200 |
wenzelm |
modernized Thy_Header;
|
file |
diff |
annotate
|
| Mon, 29 Jun 2009 16:17:57 +0200 |
haftmann |
mutual instances
|
file |
diff |
annotate
|
| Mon, 01 Jun 2009 15:26:00 +0200 |
wenzelm |
ML_Env;
|
file |
diff |
annotate
|
| Tue, 12 May 2009 19:30:33 +0200 |
haftmann |
transferred code generator preprocessor into separate module
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 19:00:29 +0100 |
wenzelm |
interpretation/interpret: prefixes within locale expression are mandatory by default;
|
file |
diff |
annotate
|
| Tue, 24 Mar 2009 15:43:37 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 11:47:05 +0100 |
wenzelm |
command 'use', 'ML': apply ML environment to theory and target as well;
|
file |
diff |
annotate
|
| Wed, 18 Mar 2009 22:41:15 +0100 |
wenzelm |
generalized ML_Context.inherit_env;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2009 17:46:49 +0100 |
wenzelm |
adapted 'method_setup' command to Method.setup;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2009 15:59:43 +0100 |
wenzelm |
added 'attribute_setup' command;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 21:44:01 +0100 |
wenzelm |
old name_spec for 'axioms' and 'defs' (from spec_parse.ML);
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 23:59:34 +0100 |
wenzelm |
added 'local_setup' command;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 22:16:50 +0100 |
wenzelm |
more uniform handling of binding in targets and derived elements;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 11:31:41 +0100 |
wenzelm |
oracle: proper name position, tuned;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 16:48:06 +0100 |
wenzelm |
discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
|
file |
diff |
annotate
|