| Sat, 24 Dec 2011 15:53:10 +0100 |
haftmann |
dropped obsolete lemma member_set
|
file |
diff |
annotate
|
| Mon, 19 Dec 2011 14:41:08 +0100 |
noschinl |
add lemmas
|
file |
diff |
annotate
|
| Thu, 15 Dec 2011 18:08:40 +0100 |
wenzelm |
clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 22:44:16 +0100 |
noschinl |
added lemmas
|
file |
diff |
annotate
|
| Fri, 09 Dec 2011 13:42:16 +0100 |
huffman |
add induction rule for list_all2
|
file |
diff |
annotate
|
| Thu, 08 Dec 2011 13:53:27 +0100 |
bulwahn |
removing special code generator setup for hd and last function because this causes problems with quickcheck narrowing as the Haskell Prelude functions throw errors that cannot be caught instead of PatternFail exceptions
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 15:41:58 +0100 |
hoelzl |
cardinality of sets of lists
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:07:10 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 08:37:27 +0200 |
bulwahn |
removing old code generator setup for lists
|
file |
diff |
annotate
|
| Mon, 03 Oct 2011 14:43:12 +0200 |
bulwahn |
adding lemma to List library for executable equation of the (refl) transitive closure
|
file |
diff |
annotate
|
| Wed, 14 Sep 2011 10:08:52 -0400 |
hoelzl |
renamed Complete_Lattices lemmas, removed legacy names
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 12:14:29 +0200 |
bulwahn |
added lemma motivated by a more specific lemma in the AFP-KBPs theories
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 13:18:27 +0200 |
blanchet |
added two lemmas about "distinct" to help Sledgehammer
|
file |
diff |
annotate
|
| Tue, 30 Aug 2011 20:10:48 +0200 |
bulwahn |
adding list_size_append (thanks to Rene Thiemann)
|
file |
diff |
annotate
|
| Tue, 30 Aug 2011 20:10:47 +0200 |
bulwahn |
strengthening list_size_pointwise (thanks to Rene Thiemann)
|
file |
diff |
annotate
|
| Fri, 26 Aug 2011 11:22:47 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 10:36:50 +0200 |
krauss |
moved recdef package to HOL/Library/Old_Recdef.thy
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 17:35:46 +0200 |
wenzelm |
modernized some simproc setup;
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 17:04:04 +0200 |
krauss |
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Fri, 20 May 2011 11:44:16 +0200 |
haftmann |
names of fold_set locales resemble name of characteristic property more closely
|
file |
diff |
annotate
|
| Sat, 14 May 2011 18:26:25 +0200 |
haftmann |
use pointfree characterisation for fold_set locale
|
file |
diff |
annotate
|
| Mon, 09 May 2011 16:11:20 +0200 |
noschinl |
add a lemma about commutative append to List.thy
|
file |
diff |
annotate
|
| Mon, 09 May 2011 12:26:25 +0200 |
noschinl |
removed assumption from lemma List.take_add
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 23:57:28 +0200 |
wenzelm |
eliminated Codegen.mode in favour of explicit argument;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +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
|
| Wed, 06 Apr 2011 23:04:00 +0200 |
wenzelm |
separate structure Term_Position;
|
file |
diff |
annotate
|