src/Pure/Isar/isar_syn.ML
Sun, 07 Nov 2010 16:39:03 +0100 wenzelm 'example_proof' is treated as non-schematic statement with irrelevant proof (NB: even regular proofs can contain unreachable parts wrt. the graph of proof promises);
Sat, 06 Nov 2010 19:36:54 +0100 wenzelm mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;
Wed, 08 Sep 2010 13:22:24 +0200 haftmann removed ancient constdefs command
Mon, 06 Sep 2010 22:31:54 +0200 wenzelm discontinued obsolete ProofContext.prems_limit;
Tue, 31 Aug 2010 23:46:49 +0200 wenzelm moved Toplevel.run_command to Pure/PIDE/document.ML;
Mon, 30 Aug 2010 11:17:05 +0200 wenzelm tuned;
Wed, 25 Aug 2010 14:18:09 +0200 wenzelm discontinued obsolete 'global' and 'local' commands;
Wed, 11 Aug 2010 16:02:03 +0200 haftmann more convenient split of class modules: class and class_declaration
Wed, 11 Aug 2010 14:45:38 +0200 haftmann renamed Theory_Target to the more appropriate Named_Target
Wed, 11 Aug 2010 14:31:43 +0200 haftmann moved instantiation target formally to class_target.ML
Wed, 11 Aug 2010 12:30:48 +0200 haftmann moved overloading target formally to overloading.ML
Sat, 31 Jul 2010 21:14:20 +0200 ballarin Interpretation in proofs supports mixins.
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;
Tue, 27 Jul 2010 23:01:42 +0200 wenzelm theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);
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;
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;
Wed, 21 Jul 2010 16:14:16 +0200 wenzelm eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing;
Tue, 20 Jul 2010 21:57:26 +0200 wenzelm warning in proper transaction context;
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
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;
Sat, 15 May 2010 23:40:00 +0200 wenzelm renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
Sat, 15 May 2010 23:32:15 +0200 wenzelm renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
Sat, 15 May 2010 23:23:45 +0200 wenzelm renamed structure ValueParse to Parse_Value;
Sat, 15 May 2010 23:16:32 +0200 wenzelm refer directly to structure Keyword and Parse;
Wed, 12 May 2010 15:25:58 +0200 wenzelm updated/unified some legacy warnings;
Thu, 29 Apr 2010 16:55:22 +0200 wenzelm ProofContext.read_const: allow for type constraint (for fixed variable);
Wed, 28 Apr 2010 12:07:52 +0200 wenzelm renamed command 'defaultsort' to 'default_sort';
Wed, 28 Apr 2010 11:41:27 +0200 wenzelm localized default sort;
Wed, 28 Apr 2010 11:09:19 +0200 wenzelm modernized/simplified Sign.set_defsort;
Mon, 26 Apr 2010 21:45:08 +0200 wenzelm command 'example_proof' opens an empty proof body;
Sun, 25 Apr 2010 15:52:03 +0200 wenzelm modernized naming conventions of main Isar proof elements;
Fri, 23 Apr 2010 22:48:07 +0200 wenzelm explicit 'schematic_theorem' etc. for schematic theorem statements;
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;
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;
Fri, 16 Apr 2010 20:17:38 +0200 wenzelm modernized old-style type abbreviations;
Fri, 16 Apr 2010 19:43:06 +0200 wenzelm local type abbreviations;
Sun, 11 Apr 2010 16:51:07 +0200 haftmann user interface for abstract datatypes is an attribute, not a command
Sun, 21 Mar 2010 19:28:25 +0100 wenzelm minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
Thu, 18 Mar 2010 22:59:44 +0100 wenzelm typedecl: no sort constraints;
Tue, 09 Mar 2010 23:32:13 +0100 wenzelm localized typedecl;
Sun, 07 Mar 2010 12:47:02 +0100 wenzelm separate structure Typedecl;
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Mon, 01 Mar 2010 17:09:42 +0100 wenzelm added type_notation command;
Wed, 24 Feb 2010 20:37:01 +0100 wenzelm allow general mixfix syntax for type constructors;
Tue, 23 Feb 2010 10:11:12 +0100 haftmann dropped axclass
Fri, 19 Feb 2010 11:06:20 +0100 haftmann added code_abstype keyword
Thu, 18 Feb 2010 23:41:01 +0100 wenzelm removed unused Theory_Target.begin;
Fri, 13 Nov 2009 21:11:15 +0100 wenzelm modernized structure Local_Theory;
Tue, 10 Nov 2009 16:04:57 +0100 wenzelm modernized structure Theory_Target;
Sun, 08 Nov 2009 14:38:36 +0100 wenzelm print_theorems: suppress concealed (global) facts, unless "!" option is given;
Thu, 05 Nov 2009 22:06:46 +0100 wenzelm allow "pervasive" local theory declarations, which are applied the background theory;
Mon, 02 Nov 2009 21:03:41 +0100 wenzelm modernized structure Proof_Node;
Wed, 28 Oct 2009 22:00:35 +0100 wenzelm provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
Thu, 01 Oct 2009 07:40:25 +0200 ballarin Merged.
Tue, 29 Sep 2009 22:15:54 +0200 ballarin Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
Tue, 01 Sep 2009 14:45:06 +0200 wenzelm modernized Thy_Header;
Mon, 29 Jun 2009 16:17:57 +0200 haftmann mutual instances
Mon, 01 Jun 2009 15:26:00 +0200 wenzelm ML_Env;
Tue, 12 May 2009 19:30:33 +0200 haftmann transferred code generator preprocessor into separate module
Thu, 26 Mar 2009 19:00:29 +0100 wenzelm interpretation/interpret: prefixes within locale expression are mandatory by default;
less more (0) -300 -100 -60 tip