QuotMain.thy
2009-10-12 Christian Urban started some strange functions
2009-10-12 Cezary Kaliszyk Further with the manual proof
2009-10-09 Cezary Kaliszyk Further experiments with proving induction manually
2009-10-09 Cezary Kaliszyk Testing if I can prove the regularized version of induction manually
2009-10-08 Christian Urban exported parts of QuotMain into a separate ML-file
2009-10-06 Christian Urban consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
2009-10-06 Christian Urban simplified typedef_quot_type_tac (using MetaSimplifier.rewrite_rule instead of the simplifier)
less more (0) -30 -10 -7 tip