Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
Thu, 15 Mar 2012 22:08:53 +0100 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
Thu, 15 Mar 2012 19:02:34 +0100 |
wenzelm |
declare minor keywords via theory header;
|
file |
diff |
annotate
|
Tue, 10 Jan 2012 23:49:53 +0100 |
berghofe |
Reverted several lemmas involving sets to the state before the
|
file |
diff |
annotate
|
Sat, 24 Dec 2011 15:53:08 +0100 |
haftmann |
treatment of type constructor `set`
|
file |
diff |
annotate
|
Wed, 30 Nov 2011 16:27:10 +0100 |
wenzelm |
prefer typedef without extra definition and alternative name;
|
file |
diff |
annotate
|
Thu, 24 Nov 2011 21:01:06 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
Thu, 08 Sep 2011 00:35:22 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
Tue, 06 Sep 2011 22:04:14 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
Mon, 05 Sep 2011 22:02:32 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Sun, 04 Sep 2011 08:43:06 +0200 |
haftmann |
pseudo-definition for perms on sets; tuned
|
file |
diff |
annotate
|
Sat, 03 Sep 2011 23:59:36 +0200 |
haftmann |
tuned specifications
|
file |
diff |
annotate
|
Sat, 03 Sep 2011 17:32:34 +0200 |
haftmann |
tuned specifications and proofs
|
file |
diff |
annotate
|
Sun, 28 Aug 2011 14:16:14 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Mon, 21 Feb 2011 17:43:23 +0100 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
Sat, 15 Jan 2011 12:38:56 +0100 |
berghofe |
Finally removed old primrec package, since Primrec.add_primrec_global
|
file |
diff |
annotate
|
Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
Wed, 29 Sep 2010 09:07:58 +0200 |
haftmann |
moved old_primrec source to nominal package, where it is still used
|
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
|
Mon, 01 Mar 2010 13:42:31 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
Wed, 24 Feb 2010 21:59:21 +0100 |
wenzelm |
proper type syntax (cf. 7425aece4ee3);
|
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
|
Mon, 21 Sep 2009 15:02:23 +0200 |
Christian Urban |
tuned some proofs
|
file |
diff |
annotate
|
Fri, 03 Jul 2009 16:51:08 +0200 |
haftmann |
nominal.ML is nominal_datatype.ML
|
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, 26 Apr 2009 23:16:24 +0200 |
Christian Urban |
reorganised the section about fresh_star and added lemma pt_fresh_star_pi
|
file |
diff |
annotate
|
Sat, 25 Apr 2009 21:42:05 +0200 |
Christian Urban |
adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
|
file |
diff |
annotate
|