Fri, 06 Apr 2012 10:37:46 +0200 | huffman | add function dest_Quotient | changeset | files |
Fri, 06 Apr 2012 13:10:45 +0200 | wenzelm | standardized alias; | changeset | files |
Fri, 06 Apr 2012 12:45:56 +0200 | wenzelm | fixed document; | changeset | files |
Fri, 06 Apr 2012 12:10:50 +0200 | wenzelm | merged | changeset | files |
Fri, 06 Apr 2012 09:35:47 +0200 | huffman | correct plumbing of proof contexts, so that force_rty_type won't generalize more type variables than it should | changeset | files |
Thu, 05 Apr 2012 23:22:54 +0200 | kuncar | detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr | changeset | files |
Thu, 05 Apr 2012 22:00:27 +0200 | kuncar | make Quotient_Def.lift_raw_const working again | changeset | files |