isabelle: Changelog

blanchet [Tue, 27 Mar 2012 16:59:13 +0300] rev 47151

tuning

blanchet [Tue, 27 Mar 2012 16:59:13 +0300] rev 47150

tuning (in particular, Symtab instead of AList)

blanchet [Tue, 27 Mar 2012 16:59:13 +0300] rev 47149

tweak slices, based on eval by Daniel Wand

blanchet [Tue, 27 Mar 2012 16:59:13 +0300] rev 47148

be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)

blanchet [Tue, 27 Mar 2012 16:59:13 +0300] rev 47147

print a hint

blanchet [Tue, 27 Mar 2012 16:59:13 +0300] rev 47146

avoid DL

blanchet [Tue, 27 Mar 2012 16:59:13 +0300] rev 47145

TFF: declare free types as types

bulwahn [Tue, 27 Mar 2012 15:34:04 +0200] rev 47144

merged

bulwahn [Tue, 27 Mar 2012 14:14:46 +0200] rev 47143

association lists with distinct keys uses the quotient infrastructure to obtain code certificates; added remarks about further improvements

huffman [Tue, 27 Mar 2012 14:49:56 +0200] rev 47142

remove redundant lemmas

isabelle