Sun, 17 Feb 2013 21:29:30 +0100 |
haftmann |
Sieve of Eratosthenes
|
file |
diff |
annotate
|
Sat, 17 Nov 2012 17:55:52 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 16 Nov 2012 18:45:57 +0100 |
hoelzl |
move theorems to be more generally useable
|
file |
diff |
annotate
|
Wed, 17 Oct 2012 14:13:57 +0200 |
bulwahn |
moving Pair_inject from legacy and duplicate section to general section, as Pair_inject was considered a duplicate in e8400e31528a by mistake (cf. communication on dev mailing list)
|
file |
diff |
annotate
|
Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
Wed, 10 Oct 2012 10:47:43 +0200 |
bulwahn |
moving simproc from Finite_Set to more appropriate Product_Type theory
|
file |
diff |
annotate
|
Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
Thu, 24 May 2012 17:25:53 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Wed, 25 Apr 2012 00:57:41 +0200 |
blanchet |
added "no_atp"s for extremely prolific, useless facts for ATPs
|
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, 23 Feb 2012 20:15:59 +0100 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
Tue, 21 Feb 2012 08:15:42 +0100 |
haftmann |
reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
|
file |
diff |
annotate
|
Mon, 20 Feb 2012 21:04:00 +0100 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
Sun, 01 Jan 2012 15:44:15 +0100 |
haftmann |
interaction of set operations for execution and membership predicate
|
file |
diff |
annotate
|
Thu, 29 Dec 2011 10:47:55 +0100 |
haftmann |
attribute code_abbrev superseedes code_unfold_post
|
file |
diff |
annotate
|
Mon, 26 Dec 2011 18:32:43 +0100 |
haftmann |
moved various set operations to theory Set (resp. Product_Type)
|
file |
diff |
annotate
|
Wed, 30 Nov 2011 18:07:14 +0100 |
wenzelm |
prefer typedef without alternative name;
|
file |
diff |
annotate
|
Wed, 30 Nov 2011 16:27:10 +0100 |
wenzelm |
prefer typedef without extra definition and alternative name;
|
file |
diff |
annotate
|
Mon, 28 Nov 2011 11:22:36 +0100 |
nipkow |
Hide Product_Type.Times - too precious an identifier
|
file |
diff |
annotate
|
Sun, 20 Nov 2011 21:07:10 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
Wed, 19 Oct 2011 17:45:25 +0200 |
huffman |
merged
|
file |
diff |
annotate
|
Tue, 18 Oct 2011 15:19:06 +0200 |
huffman |
hide typedef-generated constants Product_Type.prod and Sum_Type.sum
|
file |
diff |
annotate
|
Wed, 19 Oct 2011 08:37:22 +0200 |
bulwahn |
removing old code generator setup of inductive predicates
|
file |
diff |
annotate
|
Wed, 19 Oct 2011 08:37:21 +0200 |
bulwahn |
removing old code generator setup for product types
|
file |
diff |
annotate
|
Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
Mon, 08 Aug 2011 10:32:55 -0700 |
huffman |
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
|
file |
diff |
annotate
|
Sun, 17 Jul 2011 19:48:02 +0200 |
haftmann |
moving UNIV = ... equations to their proper theories
|
file |
diff |
annotate
|
Sat, 02 Jul 2011 22:55:58 +0200 |
haftmann |
install case certificate for If after code_datatype declaration for bool
|
file |
diff |
annotate
|
Wed, 29 Jun 2011 18:12:34 +0200 |
wenzelm |
modernized some simproc setup;
|
file |
diff |
annotate
|
Wed, 29 Jun 2011 17:35:46 +0200 |
wenzelm |
modernized some simproc setup;
|
file |
diff |
annotate
|