| Fri, 17 Aug 2018 11:26:34 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 15:05:21 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 17 Feb 2018 18:42:26 +0100 |
wenzelm |
trim context of persistent data;
|
file |
diff |
annotate
|
| Sun, 28 Jan 2018 19:28:52 +0100 |
wenzelm |
clarified take/drop/chop prefix/suffix;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 18:59:33 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2017 15:31:14 +0100 |
Lars Hupel |
strip some trailing spaces to force Pure rebuild after ce6454669360
|
file |
diff |
annotate
|
| Fri, 04 Aug 2017 08:12:37 +0200 |
haftmann |
compactified output
|
file |
diff |
annotate
|
| Thu, 03 Aug 2017 12:50:02 +0200 |
haftmann |
one single plugin for code type declarations avoids problems when bootstrapping new plugins over types which have been both declared concrete and abstract in their code historiy
|
file |
diff |
annotate
|
| Thu, 03 Aug 2017 12:50:01 +0200 |
haftmann |
uniform namespace handling for both concrete and abstract types, following 32e0da92c786
|
file |
diff |
annotate
|
| Thu, 03 Aug 2017 12:50:00 +0200 |
haftmann |
clarified
|
file |
diff |
annotate
|
| Thu, 03 Aug 2017 12:49:55 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 02 Aug 2017 20:33:39 +0200 |
haftmann |
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
|
file |
diff |
annotate
|
| Mon, 10 Jul 2017 19:48:58 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 02 Jul 2017 20:13:38 +0200 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
file |
diff |
annotate
|
| Sat, 24 Jun 2017 09:17:33 +0200 |
haftmann |
treat "undefined" constants internally as special form of case combinators
|
file |
diff |
annotate
|
| Thu, 22 Jun 2017 15:20:32 +0200 |
wenzelm |
more informative task_statistics;
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 13:07:49 +0200 |
haftmann |
deleting a code equation never leads to unimplemented function
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
do not print unimplemented functions
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
dropped void values
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
more uniform order of constructors
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
more consistent terminology
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
avoid name particle "the" where no selection is implied
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
more uniform ordering and naming of sections;
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
tuned internal signature
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
more explicit constructor name
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Mon, 05 Jun 2017 21:24:41 +0200 |
haftmann |
decomposed tuple
|
file |
diff |
annotate
|
| Mon, 05 Jun 2017 21:24:40 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 05 Jun 2017 21:24:39 +0200 |
haftmann |
clarified message
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 22:22:05 +0200 |
haftmann |
clear distinction between different situations concerning strictness of code equations
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
tuned signature
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
more correct exception handling
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
explicit tagging of code equations de-baroquifies interface
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:45 +0200 |
haftmann |
dropped unused code
|
file |
diff |
annotate
|
| Mon, 09 May 2016 14:37:47 +0200 |
wenzelm |
clarified context, notably for internal use of Simplifier;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 19:25:08 +0200 |
wenzelm |
added Thm.chyps_of;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 18:19:30 +0200 |
wenzelm |
prefer theory_id operations;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 23:40:39 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 03 Jun 2015 19:25:05 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 19:43:03 +0100 |
wenzelm |
local fixes may depend on goal params;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 28 Jan 2015 08:29:08 +0100 |
haftmann |
abstract code equation may also be default
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 21:46:41 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 21:41:29 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 20:29:30 +0200 |
wenzelm |
module Interpretation is superseded by Plugin;
|
file |
diff |
annotate
|
| Wed, 08 Oct 2014 17:37:20 +0200 |
wenzelm |
eliminated some exotic combinators;
|
file |
diff |
annotate
|
| Sun, 05 Oct 2014 20:30:58 +0200 |
haftmann |
code preprocessor tracing also for function transformers
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 22:13:23 +0200 |
haftmann |
tracing facilities for the code generator preprocessor
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 22:13:21 +0200 |
haftmann |
tuned interface
|
file |
diff |
annotate
|
| Thu, 01 May 2014 09:30:35 +0200 |
haftmann |
optional case enforcement
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:35:39 +0200 |
wenzelm |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 15:29:58 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 18:12:40 +0100 |
kuncar |
publish a useful function
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 18:12:39 +0100 |
kuncar |
add missing attributes
|
file |
diff |
annotate
|
| Sun, 09 Feb 2014 15:26:33 +0100 |
haftmann |
build up preprocessing context only once
|
file |
diff |
annotate
|
| Sun, 09 Feb 2014 15:26:33 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 01:05:46 +0100 |
haftmann |
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 01:05:30 +0100 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 01:05:30 +0100 |
haftmann |
more precise wording
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 01:05:30 +0100 |
haftmann |
uniform bookkeeping also in the case of deletion
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 22:18:31 +0100 |
haftmann |
dropped unused material
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Thu, 28 Nov 2013 08:35:14 +0100 |
haftmann |
prefer sort-stripping const_typ over Sign.the_const_type whenever appropriate
|
file |
diff |
annotate
|
| Thu, 28 Nov 2013 08:34:52 +0100 |
haftmann |
prefer name-normalizing devarify over unvarifyT whenever appropriate
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 20:35:50 +0200 |
wenzelm |
added Theory.setup convenience;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| Sun, 28 Jul 2013 05:32:02 +0200 |
haftmann |
silenced subsumption warnings for default code equations entirely
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 17:53:58 +0200 |
haftmann |
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
|
file |
diff |
annotate
|
| Fri, 28 Jun 2013 21:07:42 +0200 |
haftmann |
sort out code equations headed by a projection of a abstract datatype
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 15:30:19 +0200 |
wenzelm |
more standard module name Axclass (according to file name);
|
file |
diff |
annotate
|
| Sat, 30 Mar 2013 13:40:19 +0100 |
wenzelm |
more item markup;
|
file |
diff |
annotate
|
| Fri, 29 Mar 2013 22:14:27 +0100 |
wenzelm |
Pretty.item markup for improved readability of lists of items;
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 14:19:18 +0100 |
wenzelm |
tuned signature and module arrangement;
|
file |
diff |
annotate
|
| Thu, 07 Mar 2013 15:02:55 +0100 |
wenzelm |
tuned signature -- prefer terminology of Scala and Axiom;
|
file |
diff |
annotate
|
| Mon, 22 Oct 2012 19:02:36 +0200 |
haftmann |
close code theorems explicitly after preprocessing
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 09:17:00 +0200 |
haftmann |
no sort constraints on datatype constructors in internal bookkeeping
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 08:45:27 +0200 |
haftmann |
more consistent error messages on malformed code equations
|
file |
diff |
annotate
|
| Mon, 24 Sep 2012 19:11:35 +0200 |
haftmann |
made smlnj even happier
|
file |
diff |
annotate
|
| Sun, 23 Sep 2012 08:24:19 +0200 |
haftmann |
make smlnj happy
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 21:59:40 +0200 |
haftmann |
more strict typscheme_equiv check: must fix variables of more specific type;
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 21:59:40 +0200 |
haftmann |
cache should not contain material from descendant theory
|
file |
diff |
annotate
|
| Thu, 23 Aug 2012 13:03:29 +0200 |
wenzelm |
prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
|
file |
diff |
annotate
|
| Tue, 05 Jun 2012 10:12:54 +0200 |
haftmann |
apply preprocessing simpset also to rhs of abstract code equations
|
file |
diff |
annotate
|
| Sun, 03 Jun 2012 15:49:55 +0200 |
haftmann |
explicit check for correct number of arguments for abstract constructor
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 21:11:50 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 10:29:45 +0200 |
Andreas Lochbihler |
generalise case certificates to allow ignored parameters
|
file |
diff |
annotate
|
| Sat, 18 Feb 2012 11:31:35 +0100 |
haftmann |
more explicit error on malformed abstract equation; dropped dead code; tuned signature
|
file |
diff |
annotate
|
| Mon, 26 Dec 2011 18:32:43 +0100 |
haftmann |
dropped disfruitful `constant signatures`
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 21:36:18 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Sat, 05 Nov 2011 15:00:49 +0100 |
wenzelm |
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 23:07:48 +0200 |
haftmann |
removed some remaining artefacts of ancient SML code generator
|
file |
diff |
annotate
|
| Wed, 06 Jul 2011 20:46:06 +0200 |
wenzelm |
prefer Synchronized.var;
|
file |
diff |
annotate
|
| Sat, 02 Jul 2011 10:37:35 +0200 |
haftmann |
correction: do not assume that case const index covered all cases
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 23:31:23 +0200 |
haftmann |
remove illegal case combinators after merge
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 23:10:27 +0200 |
haftmann |
corrected misunderstanding what `old functions` are supposed to be
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 23:07:06 +0200 |
haftmann |
centralized deletion of equations for constructors; corrected misunderstanding what `old functions` are supposed to be
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 19:57:41 +0200 |
haftmann |
index cases for constructors
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 17:51:49 +0200 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|
| Fri, 06 May 2011 11:57:21 +0200 |
bulwahn |
improving merge of code specifications by removing code equations of constructors after merging two theories
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:25:25 +0200 |
wenzelm |
prefer local name spaces;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 16:45:28 +0100 |
wenzelm |
added merge_options convenience;
|
file |
diff |
annotate
|
| Sat, 08 Jan 2011 17:14:48 +0100 |
wenzelm |
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 15:03:44 +0100 |
wenzelm |
more direct use of binder_types/body_type;
|
file |
diff |
annotate
|
| Mon, 29 Nov 2010 11:38:59 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 22:01:27 +0100 |
haftmann |
typscheme with signatures is inappropriate when building empty certificate;
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 19:41:28 +0100 |
haftmann |
corrected: use canonical variables of type scheme uniformly
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 23:49:49 +0100 |
haftmann |
consider sort constraints for datatype constructors when constructing the empty equation certificate;
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 22:33:21 +0100 |
haftmann |
keep type variable arguments of datatype constructors in bookkeeping
|
file |
diff |
annotate
|
| Tue, 16 Nov 2010 10:33:36 +0100 |
haftmann |
added forall2 predicate lifter
|
file |
diff |
annotate
|
| Thu, 04 Nov 2010 17:27:38 +0100 |
haftmann |
Code.check_const etc.: reject too specific types
|
file |
diff |
annotate
|