Thu, 01 Sep 2011 13:18:27 +0200 | blanchet | added two lemmas about "distinct" to help Sledgehammer | changeset | files |
Thu, 01 Sep 2011 13:18:27 +0200 | blanchet | make "sound" sound and "unsound" more sound, based on evaluation | changeset | files |
Thu, 01 Sep 2011 16:16:25 +0900 | Cezary Kaliszyk | HOL/Import: observe distinction between sets and predicates (where possible) | changeset | files |