Tue, 24 Nov 2009 13:22:18 +0100 | blanchet | fix soundness bug in Nitpick's handling of negative literals (e.g., -1::rat) | changeset | files |
Tue, 24 Nov 2009 12:29:08 +0100 | haftmann | consisten upper/lower case | changeset | files |
Tue, 24 Nov 2009 10:33:21 +0100 | blanchet | merge | changeset | files |
Tue, 24 Nov 2009 10:33:02 +0100 | blanchet | fixed soundness bug / type error in handling of unpolarized (co)inductive predicates in Nitpick | changeset | files |
Tue, 24 Nov 2009 10:31:01 +0100 | blanchet | removed "nitpick_def" attributes from (r)trancl(p), since "Nitpick.thy" overrides these | changeset | files |
Mon, 23 Nov 2009 18:29:00 +0100 | blanchet | fix Nitpick soundness bug related to "finite (UNIV::'a set)" where "'a" is constrained by a sort to be infinite | changeset | files |