Thu, 18 Aug 2011 16:52:19 +0900 | Cezary Kaliszyk | Quotient_Examples/DList: explicit proof of remdups_eq_member_eq needed for explicit set type. | changeset | files |
Wed, 17 Aug 2011 15:12:34 -0700 | huffman | merged | changeset | files |
Wed, 17 Aug 2011 15:03:30 -0700 | huffman | HOL-IMP: respect set/pred distinction | changeset | files |
Wed, 17 Aug 2011 15:02:17 -0700 | huffman | Determinants.thy: avoid using mem_def/Collect_def | changeset | files |
Wed, 17 Aug 2011 14:42:59 -0700 | huffman | Wfrec.thy: respect set/pred distinction | changeset | files |
Thu, 18 Aug 2011 00:02:44 +0200 | wenzelm | follow updates of Isabelle/Pure; | changeset | files |