isabelle: Changelog

blanchet [Fri, 18 Nov 2011 11:47:12 +0100] rev 45556

more aggressive lambda hiding (if we anyway need to pass an option to Metis)

blanchet [Fri, 18 Nov 2011 11:47:12 +0100] rev 45555

updated Sledgehammer docs

blanchet [Fri, 18 Nov 2011 11:47:12 +0100] rev 45554

don't pass "lam_lifted" option to "metis" unless there's a good reason

blanchet [Fri, 18 Nov 2011 11:47:12 +0100] rev 45553

no needless reconstructors

blanchet [Fri, 18 Nov 2011 11:47:12 +0100] rev 45552

removed more clutter

blanchet [Fri, 18 Nov 2011 11:47:12 +0100] rev 45551

removed needless baggage

huffman [Fri, 18 Nov 2011 06:50:05 +0100] rev 45550

Word.thy: reduce usage of numeral-representation-dependent thms like number_of_is_id in proofs

huffman [Fri, 18 Nov 2011 04:56:35 +0100] rev 45549

merged

huffman [Thu, 17 Nov 2011 18:31:00 +0100] rev 45548

Groups.thy: generalize several lemmas from class ab_group_add to class group_add

huffman [Thu, 17 Nov 2011 15:07:46 +0100] rev 45547

HOL-Word: removed more duplicate theorems

isabelle