nominal2: Changelog

Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 09 Oct 2009 15:03:43 +0200] rev 72

Testing if I can prove the regularized version of induction manually

Christian Urban <urbanc@in.tum.de> [Thu, 08 Oct 2009 14:27:50 +0200] rev 71

exported parts of QuotMain into a separate ML-file

Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 15:11:30 +0200] rev 70

consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar proof of atomize_eqv.

Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 11:56:23 +0200] rev 69

simplified typedef_quot_type_tac (using MetaSimplifier.rewrite_rule instead of the simplifier)

Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 11:41:35 +0200] rev 68

renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)

Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 11:36:08 +0200] rev 67

tuned; nothing serious

Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 09:28:59 +0200] rev 66

another improvement to unlam_def

nominal2