Fri, 06 Apr 2012 13:50:07 +0200 merged
huffman [Fri, 06 Apr 2012 13:50:07 +0200] rev 47385
merged
Fri, 06 Apr 2012 10:37:46 +0200 add function dest_Quotient
huffman [Fri, 06 Apr 2012 10:37:46 +0200] rev 47384
add function dest_Quotient
Fri, 06 Apr 2012 13:10:45 +0200 standardized alias;
wenzelm [Fri, 06 Apr 2012 13:10:45 +0200] rev 47383
standardized alias;
Fri, 06 Apr 2012 12:45:56 +0200 fixed document;
wenzelm [Fri, 06 Apr 2012 12:45:56 +0200] rev 47382
fixed document;
Fri, 06 Apr 2012 12:10:50 +0200 merged
wenzelm [Fri, 06 Apr 2012 12:10:50 +0200] rev 47381
merged
Fri, 06 Apr 2012 09:35:47 +0200 correct plumbing of proof contexts, so that force_rty_type won't generalize more type variables than it should
huffman [Fri, 06 Apr 2012 09:35:47 +0200] rev 47380
correct plumbing of proof contexts, so that force_rty_type won't generalize more type variables than it should
Thu, 05 Apr 2012 23:22:54 +0200 detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar [Thu, 05 Apr 2012 23:22:54 +0200] rev 47379
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
Thu, 05 Apr 2012 22:00:27 +0200 make Quotient_Def.lift_raw_const working again
kuncar [Thu, 05 Apr 2012 22:00:27 +0200] rev 47378
make Quotient_Def.lift_raw_const working again
Thu, 05 Apr 2012 16:25:59 +0200 use standard quotient lemmas to generate transfer rules
huffman [Thu, 05 Apr 2012 16:25:59 +0200] rev 47377
use standard quotient lemmas to generate transfer rules
Thu, 05 Apr 2012 15:59:25 +0200 add transfer lemmas for quotients
huffman [Thu, 05 Apr 2012 15:59:25 +0200] rev 47376
add transfer lemmas for quotients
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip