| 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 |
| Thu, 05 Apr 2012 16:25:59 +0200 | huffman | use standard quotient lemmas to generate transfer rules | changeset | files |
| Thu, 05 Apr 2012 15:59:25 +0200 | huffman | add transfer lemmas for quotients | changeset | files |
| Thu, 05 Apr 2012 15:23:26 +0200 | huffman | define reflp directly, in the manner of symp and transp | changeset | files |
| Thu, 05 Apr 2012 14:14:16 +0200 | huffman | set up and use lift_definition for word operations | changeset | files |
| Thu, 05 Apr 2012 12:18:06 +0200 | huffman | lift_definition declares transfer_rule attribute | changeset | files |
| Thu, 05 Apr 2012 10:48:46 +0200 | huffman | configure transfer method for 'a word -> int | changeset | files |