| 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
|
| Thu, 05 Apr 2012 08:43:31 +0200 |
krauss |
added timestamps to logging of named thms
|
changeset |
files
|
| Thu, 05 Apr 2012 08:13:40 +0200 |
huffman |
merged
|
changeset |
files
|
| Wed, 04 Apr 2012 20:45:19 +0200 |
huffman |
merged
|
changeset |
files
|
| Wed, 04 Apr 2012 16:48:39 +0200 |
huffman |
add lemmas for generating transfer rules for typedefs
|
changeset |
files
|