| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
tuned structure inclusion
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 18:19:57 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 15:58:27 +0100 |
wenzelm |
avoid hard-wired theory names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 10:45:03 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 22:30:58 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:37:06 +0100 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
use names like 'rec_mytype' and 'case_mytype' in old datatype package as well, to avoid a mixture
|
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
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| Sat, 27 Apr 2013 20:50:20 +0200 |
wenzelm |
uniform Proof.context for hyp_subst_tac;
|
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, 27 Mar 2013 14:19:18 +0100 |
wenzelm |
tuned signature and module arrangement;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 21:22:35 +0200 |
wenzelm |
discontinued typedef with alternative name;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 15:08:29 +0200 |
wenzelm |
discontinued typedef with implicit set_def;
|
file |
diff |
annotate
|
| Wed, 05 Sep 2012 19:51:00 +0200 |
wenzelm |
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 20:07:00 +0100 |
wenzelm |
prefer formally checked @{keyword} parser;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 20:04:24 +0100 |
wenzelm |
more explicit indication of def names;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 21:16:15 +0100 |
wenzelm |
discontinued old-style Term.list_abs in favour of plain Term.abs;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 20:05:58 +0100 |
wenzelm |
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
|
file |
diff |
annotate
|
| Sat, 17 Dec 2011 15:09:11 +0100 |
wenzelm |
eliminated Drule.export_without_context which is not really required here;
|
file |
diff |
annotate
|
| Sat, 17 Dec 2011 13:08:03 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 16 Dec 2011 21:23:21 +0100 |
wenzelm |
eliminated old-fashioned Global_Theory.add_thms(s);
|
file |
diff |
annotate
|
| Thu, 15 Dec 2011 17:37:14 +0100 |
wenzelm |
separate rep_datatype.ML;
|
file |
diff |
annotate
|
| Thu, 15 Dec 2011 14:11:57 +0100 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 21:54:32 +0100 |
wenzelm |
avoid fragile Sign.intern_const -- pass internal names directly;
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 20:36:17 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 15:30:17 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 23:23:51 +0100 |
wenzelm |
'datatype' specifications allow explicit sort constraints;
|
file |
diff |
annotate
|
| Mon, 12 Dec 2011 23:05:21 +0100 |
wenzelm |
datatype dtyp with explicit sort information;
|
file |
diff |
annotate
|
| Mon, 12 Dec 2011 20:55:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 16:37:35 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 16:24:48 +0100 |
wenzelm |
some localization;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 14:54:25 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 14:26:43 +0100 |
wenzelm |
eliminated some legacy operations;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 13:38:24 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 23:30:08 +0100 |
wenzelm |
discontinued obsolete datatype "alt_names";
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 21:14:01 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2011 11:27:21 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 18:05:31 +0200 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 21:42:47 +0200 |
wenzelm |
added Binding.print convenience, which includes quote already;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
| Thu, 30 Dec 2010 23:42:06 +0100 |
wenzelm |
do not open auxiliary ML structures;
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 10:03:13 +0100 |
huffman |
theorem names generated by the (rep_)datatype command now have mandatory qualifiers
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 21:09:36 +0100 |
wenzelm |
keep private things private, without comments;
|
file |
diff |
annotate
|
| Thu, 28 Oct 2010 22:12:08 +0200 |
wenzelm |
preserve original source position of exn;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 16:54:44 +0200 |
haftmann |
"prod" and "sum" replace "*" and "+" respectively
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 15:38:58 +0200 |
wenzelm |
spelling;
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 21:38:38 +0100 |
wenzelm |
Typedef.info: separate global and local part, only the latter is transformed by morphisms;
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 00:47:23 +0100 |
wenzelm |
typedef etc.: no constraints;
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 14:43:04 +0100 |
wenzelm |
global typedef;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 23:51:31 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 20:57:08 +0100 |
wenzelm |
clarified @{const_name} vs. @{const_abbrev};
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 22:32:09 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 20:37:01 +0100 |
wenzelm |
allow general mixfix syntax for type constructors;
|
file |
diff |
annotate
|
| Mon, 15 Feb 2010 17:17:51 +0100 |
wenzelm |
discontinued unnamed infix syntax;
|
file |
diff |
annotate
|
| Sun, 07 Feb 2010 19:33:34 +0100 |
wenzelm |
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
|
file |
diff |
annotate
|
| Mon, 30 Nov 2009 12:28:12 +0100 |
haftmann |
dropped some unused bindings
|
file |
diff |
annotate
|
| Mon, 30 Nov 2009 11:42:49 +0100 |
haftmann |
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
|
file |
diff |
annotate
|
| Fri, 27 Nov 2009 08:41:10 +0100 |
haftmann |
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 11:16:57 +0100 |
haftmann |
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| Sun, 01 Nov 2009 15:24:45 +0100 |
wenzelm |
modernized structure Rule_Cases;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:15:33 +0100 |
wenzelm |
modernized functor/structures Interpretation;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:09:41 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 13:21:38 +0100 |
wenzelm |
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 22:55:27 +0100 |
wenzelm |
Datatype.read_typ: standard argument order;
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 10:52:07 +0200 |
haftmann |
dropped Datatype.distinct_simproc
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 10:15:31 +0200 |
haftmann |
removed old-style \ and \\ infixes
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Tue, 13 Oct 2009 14:08:01 +0200 |
haftmann |
deactivated Datatype.distinct_simproc
|
file |
diff |
annotate
|
| Tue, 13 Oct 2009 08:36:39 +0200 |
haftmann |
more appropriate abstraction over distinctness rules
|
file |
diff |
annotate
|
| Mon, 12 Oct 2009 15:26:40 +0200 |
haftmann |
dropped dist_ss
|
file |
diff |
annotate
|
| Mon, 12 Oct 2009 13:40:28 +0200 |
haftmann |
dropped rule duplicates
|
file |
diff |
annotate
|
| Mon, 12 Oct 2009 10:24:07 +0200 |
haftmann |
dropped redundancy
|
file |
diff |
annotate
|
| Fri, 09 Oct 2009 13:34:40 +0200 |
haftmann |
dropped simproc_dist formally
|
file |
diff |
annotate
|
| Thu, 08 Oct 2009 19:33:03 +0200 |
haftmann |
lookup for datatype constructors considers type annotations to resolve overloading
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 15:25:43 +0200 |
haftmann |
less auxiliary functions
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 14:54:15 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 14:48:30 +0200 |
haftmann |
shared code between rep_datatype and datatype
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 10:51:12 +0200 |
haftmann |
further unification of datatype and rep_datatype
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 10:20:21 +0200 |
haftmann |
avoid compound fields in datatype info record
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 09:47:18 +0200 |
haftmann |
explicit pointless checkpoint
|
file |
diff |
annotate
|
| Sun, 27 Sep 2009 20:58:25 +0200 |
haftmann |
emerging common infrastructure for datatype and rep_datatype
|
file |
diff |
annotate
|
| Sun, 27 Sep 2009 20:43:47 +0200 |
haftmann |
streamlined rep_datatype further
|
file |
diff |
annotate
|
| Sun, 27 Sep 2009 20:34:50 +0200 |
haftmann |
simplified rep_datatype
|
file |
diff |
annotate
|
| Sun, 27 Sep 2009 20:19:56 +0200 |
haftmann |
more appropriate order of field in dt_info
|
file |
diff |
annotate
|
| Sun, 27 Sep 2009 20:15:45 +0200 |
haftmann |
re-established reasonable inner outline for module
|
file |
diff |
annotate
|
| Sun, 27 Sep 2009 09:52:23 +0200 |
haftmann |
registering split rules and projected induction rules; ML identifiers more close to Isar theorem names
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
adapted configuration for DatatypeCase.make_case
|
file |
diff |
annotate
|
| Fri, 14 Aug 2009 15:36:57 +0200 |
haftmann |
inserted space into message
|
file |
diff |
annotate
|
| Fri, 24 Jul 2009 18:58:58 +0200 |
wenzelm |
renamed functor ProjectRuleFun to Project_Rule;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 15:52:30 +0200 |
haftmann |
dropped ancient flat_names option
|
file |
diff |
annotate
|
| Mon, 29 Jun 2009 16:17:56 +0200 |
haftmann |
canonical prefix for datatype derivates
|
file |
diff |
annotate
|
| Wed, 24 Jun 2009 21:28:02 +0200 |
wenzelm |
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 16:27:12 +0200 |
haftmann |
tuned interfaces of datatype module
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 15:32:34 +0200 |
haftmann |
add_datatypes does not yield particular rules any longer
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 14:50:34 +0200 |
haftmann |
add_datatype interface yields type names and less rules
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
| base
|