Sat, 24 Dec 2011 15:53:11 +0100 | haftmann | added setup for executable code | changeset | files |
Sat, 24 Dec 2011 15:53:11 +0100 | haftmann | moved `sublists` to theory Enum | changeset | files |
Sat, 24 Dec 2011 15:53:11 +0100 | haftmann | commented out examples which choke on strict set/pred distinction | changeset | files |
Sat, 24 Dec 2011 15:53:11 +0100 | haftmann | explicitly spelt out proof of equivariance avoids problem with automation due to type constructor `set` | changeset | files |
Sat, 24 Dec 2011 15:53:10 +0100 | haftmann | adjusted to set/pred distinction by means of type constructor `set` | changeset | files |
Sat, 24 Dec 2011 15:53:10 +0100 | haftmann | dropped references to obsolete fact `mem_def` | changeset | files |
Sat, 24 Dec 2011 15:53:10 +0100 | haftmann | dropped obsolete lemma member_set | changeset | files |