Tue, 28 Jun 2011 10:52:15 +0200collapse map functions with identity subcoercions to identities;
traytel [Tue, 28 Jun 2011 10:52:15 +0200] rev 44462
collapse map functions with identity subcoercions to identities;

Tue, 28 Jun 2011 21:06:59 +0200reenabled accidentally-disabled automatic minimization
blanchet [Tue, 28 Jun 2011 21:06:59 +0200] rev 44461
reenabled accidentally-disabled automatic minimization

Tue, 28 Jun 2011 20:42:29 +0200tuned markup;
wenzelm [Tue, 28 Jun 2011 20:42:29 +0200] rev 44460
tuned markup;

Tue, 28 Jun 2011 17:13:32 +0100merged
paulson [Tue, 28 Jun 2011 17:13:32 +0100] rev 44459
merged

Tue, 28 Jun 2011 17:12:50 +0100tidied messy proofs
paulson [Tue, 28 Jun 2011 17:12:50 +0100] rev 44458
tidied messy proofs

Tue, 28 Jun 2011 16:43:44 +0200merged
bulwahn [Tue, 28 Jun 2011 16:43:44 +0200] rev 44457
merged

Tue, 28 Jun 2011 14:36:43 +0200adding timeout to quickcheck narrowing
bulwahn [Tue, 28 Jun 2011 14:36:43 +0200] rev 44456
adding timeout to quickcheck narrowing

Tue, 28 Jun 2011 14:52:46 +0100simplified proofs using metis calls
paulson [Tue, 28 Jun 2011 14:52:46 +0100] rev 44455
simplified proofs using metis calls

Tue, 28 Jun 2011 12:48:00 +0100merged
paulson [Tue, 28 Jun 2011 12:48:00 +0100] rev 44454
merged

Tue, 28 Jun 2011 12:47:32 +0100keyfree: The set of key-free messages (and associated theorems)
paulson [Tue, 28 Jun 2011 12:47:32 +0100] rev 44453
keyfree: The set of key-free messages (and associated theorems)