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
Thu, 05 Apr 2012 15:23:26 +0200 define reflp directly, in the manner of symp and transp
huffman [Thu, 05 Apr 2012 15:23:26 +0200] rev 47375
define reflp directly, in the manner of symp and transp
Thu, 05 Apr 2012 14:14:16 +0200 set up and use lift_definition for word operations
huffman [Thu, 05 Apr 2012 14:14:16 +0200] rev 47374
set up and use lift_definition for word operations
Thu, 05 Apr 2012 12:18:06 +0200 lift_definition declares transfer_rule attribute
huffman [Thu, 05 Apr 2012 12:18:06 +0200] rev 47373
lift_definition declares transfer_rule attribute
Thu, 05 Apr 2012 10:48:46 +0200 configure transfer method for 'a word -> int
huffman [Thu, 05 Apr 2012 10:48:46 +0200] rev 47372
configure transfer method for 'a word -> int
Thu, 05 Apr 2012 08:43:31 +0200 added timestamps to logging of named thms
krauss [Thu, 05 Apr 2012 08:43:31 +0200] rev 47371
added timestamps to logging of named thms
Thu, 05 Apr 2012 08:13:40 +0200 merged
huffman [Thu, 05 Apr 2012 08:13:40 +0200] rev 47370
merged
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip