Mon, 29 Apr 2013 13:41:34 +0200 | blanchet | removed unreferenced thm | changeset | files |
Mon, 29 Apr 2013 13:40:26 +0200 | blanchet | tuned function signatures | changeset | files |
Mon, 29 Apr 2013 11:46:03 +0200 | blanchet | factored out derivation of coinduction, unfold, corec | changeset | files |
Mon, 29 Apr 2013 11:04:56 +0200 | blanchet | code tuning | changeset | files |
Mon, 29 Apr 2013 10:37:23 +0200 | blanchet | factored out derivation of induction principles, folds and recs, in preparation for reduction of nested to mutual | changeset | files |
Mon, 29 Apr 2013 11:31:40 +0200 | nipkow | tuned | changeset | files |