nominal2: Changelog

Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 03:48:39 +0100] rev 684

added an attempt to get a finite set theory

Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 03:47:10 +0100] rev 683

removed memb and used standard mem (member from List.thy)

Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 03:25:42 +0100] rev 682

merged

Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 03:11:19 +0100] rev 681

simplified proofs

Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 02:46:08 +0100] rev 680

removed quot_respect attribute of a non-standard lemma

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 10 Dec 2009 02:42:09 +0100] rev 679

With int_of_nat as a quotient_def, lemmas about it can be easily lifted.

Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 01:48:39 +0100] rev 678

merged

Christian Urban <urbanc@in.tum.de> [Thu, 10 Dec 2009 01:47:55 +0100] rev 677

naming in this file cannot be made to agree to the original (PROBLEM?)

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 10 Dec 2009 01:39:47 +0100] rev 676

Lifted some kind of induction.

Christian Urban <urbanc@in.tum.de> [Wed, 09 Dec 2009 23:32:16 +0100] rev 675

more proofs in IntEx2

nominal2