src/Pure/ML/ml_thms.ML
Fri, 23 Feb 2018 21:27:20 +0100 wenzelm tuned signature;
Wed, 06 Dec 2017 18:59:33 +0100 wenzelm prefer control symbol antiquotations;
Mon, 12 Jun 2017 11:32:23 +0200 wenzelm more markup for HTML rendering;
Mon, 23 May 2016 21:30:30 +0200 wenzelm embedded content may be delimited via cartouches;
Thu, 07 Apr 2016 13:54:02 +0200 wenzelm simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
Tue, 05 Apr 2016 20:03:24 +0200 wenzelm clarified modules -- simplified bootstrap;
Wed, 09 Dec 2015 16:36:26 +0100 wenzelm clarified type Token.src: plain token list, with usual implicit value assignment;
Wed, 10 Dec 2014 19:24:54 +0100 wenzelm more careful handling of auxiliary environment structure -- allow nested ML evaluation;
Mon, 08 Dec 2014 22:42:12 +0100 wenzelm expand ML cartouches to Input.source;
Sat, 01 Nov 2014 20:19:07 +0100 wenzelm clarified syntax -- avoid overlap with command category;
Mon, 25 Aug 2014 12:58:20 +0200 wenzelm tuned signature;
Fri, 22 Aug 2014 15:39:30 +0200 wenzelm tuned whitespace;
Thu, 21 Aug 2014 22:48:39 +0200 wenzelm tuned signature -- define some elementary operations earlier;
Tue, 19 Aug 2014 23:17:51 +0200 wenzelm tuned signature -- moved type src to Token, without aliases;
Thu, 27 Mar 2014 17:56:13 +0100 wenzelm redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
Tue, 25 Mar 2014 13:18:10 +0100 wenzelm added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
Tue, 18 Mar 2014 16:16:28 +0100 wenzelm clarified modules;
Tue, 18 Mar 2014 11:07:47 +0100 wenzelm tuned signature -- rearranged modules;
Wed, 12 Mar 2014 22:57:50 +0100 wenzelm tuned signature -- clarified module name;
Wed, 12 Mar 2014 21:58:48 +0100 wenzelm simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
Sat, 08 Mar 2014 21:08:10 +0100 wenzelm modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
Wed, 05 Mar 2014 13:11:08 +0100 wenzelm clarified init_assignable: make double-sure that initial values are reset;
Fri, 28 Feb 2014 10:40:04 +0100 wenzelm more explicit method reports;
Wed, 26 Feb 2014 11:14:38 +0100 wenzelm tuned;
Wed, 26 Feb 2014 10:40:13 +0100 wenzelm method language markup, e.g. relevant to prevent outer keyword completion;
Sun, 16 Feb 2014 17:25:03 +0100 wenzelm prefer user-space tool within Pure.thy;
Sun, 16 Feb 2014 17:17:26 +0100 wenzelm more markup;
Wed, 22 Jan 2014 16:03:11 +0100 wenzelm tuned signature;
Tue, 31 Dec 2013 14:29:16 +0100 wenzelm proper context for norm_hhf and derived operations;
Fri, 23 Aug 2013 20:35:50 +0200 wenzelm added Theory.setup convenience;
Fri, 23 Aug 2013 19:53:27 +0200 wenzelm clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
Fri, 23 Aug 2013 17:01:12 +0200 wenzelm tuned signature;
Sun, 12 Aug 2012 22:39:28 +0200 wenzelm tuned;
Sun, 12 Aug 2012 20:45:34 +0200 wenzelm more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
Sat, 11 Aug 2012 22:17:46 +0200 wenzelm faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
Fri, 27 Apr 2012 22:47:30 +0200 wenzelm clarified signature;
Sat, 19 Nov 2011 21:18:38 +0100 wenzelm added ML antiquotation @{attributes};
Wed, 19 Oct 2011 17:03:07 +0200 wenzelm proper source positions for @{lemma};
Mon, 27 Jun 2011 16:53:31 +0200 wenzelm ML antiquotations are managed as theory data, with proper name space and entity markup;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Sun, 09 Jan 2011 21:33:41 +0100 wenzelm reverted 08240feb69c7 -- breaks positions of reports;
Tue, 21 Dec 2010 21:05:50 +0100 wenzelm more robust ML antiquotations -- allow original tokens without adjacent whitespace;
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
Sat, 15 May 2010 23:16:32 +0200 wenzelm refer directly to structure Keyword and Parse;
Sun, 25 Apr 2010 15:52:03 +0200 wenzelm modernized naming conventions of main Isar proof elements;
Sun, 07 Feb 2010 18:04:48 +0100 wenzelm simplified interface for ML antiquotations, struct_name is always "Isabelle";
Sun, 15 Nov 2009 19:45:05 +0100 wenzelm eliminated obsolete thm position tags;
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Wed, 04 Mar 2009 23:05:32 +0100 wenzelm ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Thu, 14 Aug 2008 16:52:56 +0200 wenzelm ML_Context.add_antiq: pass position;
Sat, 09 Aug 2008 22:43:46 +0200 wenzelm unified Args.T with OuterLex.token, renamed some operations;
Thu, 10 Jul 2008 13:37:34 +0200 wenzelm @{lemma}: allow terminal method, close derivation unless (open) mode is given;
Sat, 28 Jun 2008 22:52:07 +0200 wenzelm Isar theorem values within ML.
less more (0) tip