src/Pure/Isar/code.ML
Tue, 20 Jun 2017 08:01:56 +0200 haftmann tuned whitespace
Mon, 05 Jun 2017 21:24:41 +0200 haftmann decomposed tuple
Mon, 05 Jun 2017 21:24:40 +0200 haftmann tuned
Mon, 05 Jun 2017 21:24:39 +0200 haftmann clarified message
Sat, 29 Oct 2016 00:39:33 +0200 blanchet avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar
Mon, 06 Jun 2016 22:22:05 +0200 haftmann clear distinction between different situations concerning strictness of code equations
Mon, 06 Jun 2016 21:28:46 +0200 haftmann tuned signature
Mon, 06 Jun 2016 21:28:46 +0200 haftmann more correct exception handling
Mon, 06 Jun 2016 21:28:46 +0200 haftmann explicit tagging of code equations de-baroquifies interface
Mon, 06 Jun 2016 21:28:45 +0200 haftmann dropped unused code
Mon, 09 May 2016 14:37:47 +0200 wenzelm clarified context, notably for internal use of Simplifier;
Fri, 25 Sep 2015 20:37:59 +0200 wenzelm moved remaining display.ML to more_thm.ML;
Sun, 16 Aug 2015 19:25:08 +0200 wenzelm added Thm.chyps_of;
Sun, 16 Aug 2015 18:19:30 +0200 wenzelm prefer theory_id operations;
Mon, 27 Jul 2015 23:40:39 +0200 wenzelm tuned signature;
Wed, 03 Jun 2015 19:25:05 +0200 wenzelm clarified context;
Mon, 23 Mar 2015 19:43:03 +0100 wenzelm local fixes may depend on goal params;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 28 Jan 2015 08:29:08 +0100 haftmann abstract code equation may also be default
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Mon, 13 Oct 2014 21:46:41 +0200 wenzelm tuned signature;
Mon, 13 Oct 2014 21:41:29 +0200 wenzelm tuned signature;
Mon, 13 Oct 2014 20:29:30 +0200 wenzelm module Interpretation is superseded by Plugin;
Wed, 08 Oct 2014 17:37:20 +0200 wenzelm eliminated some exotic combinators;
Sun, 05 Oct 2014 20:30:58 +0200 haftmann code preprocessor tracing also for function transformers
Tue, 19 Aug 2014 23:17:51 +0200 wenzelm tuned signature -- moved type src to Token, without aliases;
Sat, 28 Jun 2014 22:13:23 +0200 haftmann tracing facilities for the code generator preprocessor
Sat, 28 Jun 2014 22:13:21 +0200 haftmann tuned interface
Thu, 01 May 2014 09:30:35 +0200 haftmann optional case enforcement
Thu, 03 Apr 2014 10:51:22 +0200 blanchet use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
Mon, 31 Mar 2014 12:35:39 +0200 wenzelm some shortcuts for chunks, which sometimes avoid bulky string output;
Tue, 18 Mar 2014 15:29:58 +0100 wenzelm more antiquotations;
Mon, 24 Feb 2014 18:12:40 +0100 kuncar publish a useful function
Mon, 24 Feb 2014 18:12:39 +0100 kuncar don't be so aggresive for a public test function and raise only BAD_THM instead of ERROR
Mon, 24 Feb 2014 18:12:39 +0100 kuncar add missing attributes
Sun, 09 Feb 2014 15:26:33 +0100 haftmann build up preprocessing context only once
Sun, 09 Feb 2014 15:26:33 +0100 haftmann tuned
Wed, 01 Jan 2014 01:05:46 +0100 haftmann explicit distinction between empty code equations and no code equations, including convenient declaration attributes
Wed, 01 Jan 2014 01:05:30 +0100 haftmann tuned whitespace
Wed, 01 Jan 2014 01:05:30 +0100 haftmann more precise wording
Wed, 01 Jan 2014 01:05:30 +0100 haftmann uniform bookkeeping also in the case of deletion
Tue, 31 Dec 2013 22:18:31 +0100 haftmann dropped unused material
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Thu, 28 Nov 2013 08:35:14 +0100 haftmann prefer sort-stripping const_typ over Sign.the_const_type whenever appropriate
Thu, 28 Nov 2013 08:34:52 +0100 haftmann prefer name-normalizing devarify over unvarifyT whenever appropriate
Fri, 23 Aug 2013 20:35:50 +0200 wenzelm added Theory.setup convenience;
Tue, 30 Jul 2013 15:09:25 +0200 wenzelm type theory is purely value-oriented;
Sun, 28 Jul 2013 05:32:02 +0200 haftmann silenced subsumption warnings for default code equations entirely
Sat, 13 Jul 2013 17:53:58 +0200 haftmann attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
Fri, 28 Jun 2013 21:07:42 +0200 haftmann sort out code equations headed by a projection of a abstract datatype
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 10 Apr 2013 15:30:19 +0200 wenzelm more standard module name Axclass (according to file name);
Sat, 30 Mar 2013 13:40:19 +0100 wenzelm more item markup;
Fri, 29 Mar 2013 22:14:27 +0100 wenzelm Pretty.item markup for improved readability of lists of items;
Wed, 27 Mar 2013 14:19:18 +0100 wenzelm tuned signature and module arrangement;
Thu, 07 Mar 2013 15:02:55 +0100 wenzelm tuned signature -- prefer terminology of Scala and Axiom;
Mon, 22 Oct 2012 19:02:36 +0200 haftmann close code theorems explicitly after preprocessing
Thu, 18 Oct 2012 09:17:00 +0200 haftmann no sort constraints on datatype constructors in internal bookkeeping
Wed, 10 Oct 2012 08:45:27 +0200 haftmann more consistent error messages on malformed code equations
Mon, 24 Sep 2012 19:11:35 +0200 haftmann made smlnj even happier
less more (0) -100 -60 tip