Wed, 07 Oct 2015 10:02:43 +0200 | blanchet | disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier | changeset | files |
Tue, 06 Oct 2015 21:04:44 +0200 | blanchet | avoid unsound 'nitpick_simp' attribute on nonterminating, nonproductive equations | changeset | files |