| Sat, 21 Apr 2012 21:38:08 +0200 |
huffman |
update NEWS for transfer/quotient
|
changeset |
files
|
| Sat, 21 Apr 2012 20:52:33 +0200 |
huffman |
enable variant of transfer method that proves an implication instead of an equivalence
|
changeset |
files
|
| Thu, 19 Apr 2012 19:36:24 +0200 |
haftmann |
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
|
changeset |
files
|
| Sat, 21 Apr 2012 15:26:05 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 21 Apr 2012 13:54:29 +0200 |
huffman |
NEWS for transfer, lifting, and quotient
|
changeset |
files
|
| Sat, 21 Apr 2012 13:49:31 +0200 |
huffman |
new example theory for transfer package
|
changeset |
files
|
| Sat, 21 Apr 2012 14:53:04 +0200 |
wenzelm |
some builtin session timing;
|
changeset |
files
|
| Sat, 21 Apr 2012 13:12:27 +0200 |
huffman |
move alternative definition lemmas into Lifting.thy;
|
changeset |
files
|
| Sat, 21 Apr 2012 13:06:22 +0200 |
huffman |
tuned proofs
|
changeset |
files
|
| Sat, 21 Apr 2012 11:21:23 +0200 |
huffman |
add transfer rule for List.set
|
changeset |
files
|
| Sat, 21 Apr 2012 11:04:21 +0200 |
huffman |
remove duplicate of lemma id_transfer
|
changeset |
files
|
| Sat, 21 Apr 2012 11:02:01 +0200 |
huffman |
added covariant relator set_rel, with transfer rules for set operations
|
changeset |
files
|