Wed, 09 Sep 2015 20:57:21 +0200 |
wenzelm |
simplified simproc programming interfaces;
|
file |
diff |
annotate
|
Sat, 18 Jul 2015 20:54:56 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
Fri, 06 Mar 2015 23:57:01 +0100 |
wenzelm |
clarified context;
|
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, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
Wed, 29 Oct 2014 17:01:44 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
Wed, 17 Sep 2014 08:23:53 +0200 |
blanchet |
support (finite values of) codatatypes in Quickcheck
|
file |
diff |
annotate
|
Wed, 03 Sep 2014 00:06:28 +0200 |
blanchet |
removed vacuous theorem references
|
file |
diff |
annotate
|
Wed, 03 Sep 2014 00:06:22 +0200 |
blanchet |
ported 'Statespace' to support new datatypes as well
|
file |
diff |
annotate
|
Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
|
file |
diff |
annotate
|
Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
tuned structure inclusion
|
file |
diff |
annotate
|
Fri, 07 Mar 2014 11:34:41 +0100 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
Fri, 14 Feb 2014 07:53:45 +0100 |
blanchet |
merged 'List.map' and 'List.list.map'
|
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
|
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
|
Fri, 02 Dec 2011 14:54:25 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Mon, 28 Nov 2011 17:06:29 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Wed, 23 Nov 2011 22:59:39 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
Sun, 06 Nov 2011 18:42:15 +0100 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
Sun, 06 Nov 2011 17:05:45 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 24 Mar 2011 16:56:19 +0100 |
wenzelm |
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
|
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
|
Fri, 17 Dec 2010 16:25:21 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Mon, 06 Sep 2010 19:13:10 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
Wed, 25 Aug 2010 18:36:22 +0200 |
wenzelm |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
Thu, 19 Aug 2010 16:08:59 +0200 |
haftmann |
tuned quotes
|
file |
diff |
annotate
|
Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
Tue, 27 Jul 2010 17:09:35 +0200 |
haftmann |
delete structure Basic_Record; avoid `record` in names in structure Record
|
file |
diff |
annotate
|
Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
Thu, 15 Apr 2010 15:38:58 +0200 |
wenzelm |
spelling;
|
file |
diff |
annotate
|
Sun, 28 Mar 2010 16:29:51 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 28 Feb 2010 23:51:31 +0100 |
wenzelm |
more antiquotations;
|
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
|
Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
Mon, 19 Oct 2009 23:02:23 +0200 |
wenzelm |
eliminated duplicate fold1 -- beware of argument order!
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 00:52:37 +0200 |
wenzelm |
explicitly qualify Drule.standard;
|
file |
diff |
annotate
|
Thu, 15 Oct 2009 23:28:10 +0200 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
Tue, 13 Oct 2009 14:08:00 +0200 |
haftmann |
dropped Datatype.distinct_simproc; tuned
|
file |
diff |
annotate
|
Wed, 15 Jul 2009 23:48:21 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Tue, 23 Jun 2009 16:27:12 +0200 |
haftmann |
tuned interfaces of datatype module
|
file |
diff |
annotate
|
Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
Sun, 15 Mar 2009 15:59:44 +0100 |
wenzelm |
simplified attribute setup;
|
file |
diff |
annotate
|
Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
Thu, 05 Mar 2009 20:17:02 +0100 |
wenzelm |
removed spurious occurrences of old rep_ss;
|
file |
diff |
annotate
|
Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
Thu, 01 Jan 2009 23:31:49 +0100 |
wenzelm |
normalized some ML type/val aliases;
|
file |
diff |
annotate
|
Wed, 10 Dec 2008 22:55:15 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Mon, 22 Sep 2008 08:00:24 +0200 |
haftmann |
fixed headers
|
file |
diff |
annotate
|
Mon, 23 Jun 2008 23:45:39 +0200 |
wenzelm |
Logic.all/mk_equals/mk_implies;
|
file |
diff |
annotate
|
Mon, 09 Jun 2008 17:31:25 +0200 |
wenzelm |
DatatypePackage.distinct_simproc;
|
file |
diff |
annotate
|
Sat, 29 Mar 2008 22:55:49 +0100 |
wenzelm |
purely functional setup of claset/simpset/clasimpset;
|
file |
diff |
annotate
|
Mon, 12 Nov 2007 11:07:22 +0100 |
schirmer |
added signatures;
|
file |
diff |
annotate
|
Wed, 24 Oct 2007 18:36:09 +0200 |
schirmer |
added Statespace library
|
file |
diff |
annotate
|