Thu, 10 Dec 2009 04:23:13 +0100 | Christian Urban | moved the interpretation code into Unused.thy | changeset | files |
Thu, 10 Dec 2009 03:48:39 +0100 | Christian Urban | added an attempt to get a finite set theory | changeset | files |
Thu, 10 Dec 2009 03:47:10 +0100 | Christian Urban | removed memb and used standard mem (member from List.thy) | changeset | files |
Thu, 10 Dec 2009 03:25:42 +0100 | Christian Urban | merged | changeset | files |
Thu, 10 Dec 2009 03:11:19 +0100 | Christian Urban | simplified proofs | changeset | files |
Thu, 10 Dec 2009 02:46:08 +0100 | Christian Urban | removed quot_respect attribute of a non-standard lemma | changeset | files |
Thu, 10 Dec 2009 02:42:09 +0100 | Cezary Kaliszyk | With int_of_nat as a quotient_def, lemmas about it can be easily lifted. | changeset | files |