nominal2: File revisions

QuotMain.thy

Mon, 12 Oct 2009 14:30:50 +0200	Christian Urban	started some strange functions	file \| diff \| annotate
Mon, 12 Oct 2009 13:58:31 +0200	Cezary Kaliszyk	Further with the manual proof	file \| diff \| annotate
Fri, 09 Oct 2009 17:05:45 +0200	Cezary Kaliszyk	Further experiments with proving induction manually	file \| diff \| annotate
Fri, 09 Oct 2009 15:03:43 +0200	Cezary Kaliszyk	Testing if I can prove the regularized version of induction manually	file \| diff \| annotate
Thu, 08 Oct 2009 14:27:50 +0200	Christian Urban	exported parts of QuotMain into a separate ML-file	file \| diff \| annotate
Tue, 06 Oct 2009 15:11:30 +0200	Christian Urban	consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar	file \| diff \| annotate
Tue, 06 Oct 2009 11:56:23 +0200	Christian Urban	simplified typedef_quot_type_tac (using MetaSimplifier.rewrite_rule instead of the simplifier)	file \| diff \| annotate
Tue, 06 Oct 2009 11:41:35 +0200	Christian Urban	renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)	file \| diff \| annotate

nominal2