Fri, 27 Sep 2013 14:43:26 +0200 |
kuncar |
allow to specify multiple parametricity transfer rules in lift_definition
|
changeset |
files
|
Fri, 27 Sep 2013 12:26:39 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
Fri, 27 Sep 2013 12:26:23 +0200 |
Andreas Lochbihler |
generalise lemma
|
changeset |
files
|
Fri, 27 Sep 2013 11:56:52 +0200 |
wenzelm |
proper latex;
|
changeset |
files
|
Fri, 27 Sep 2013 10:40:02 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
Fri, 27 Sep 2013 09:26:31 +0200 |
Andreas Lochbihler |
add relator for 'a filter and parametricity theorems
|
changeset |
files
|
Fri, 27 Sep 2013 09:15:40 +0200 |
Andreas Lochbihler |
tuned proofs
|
changeset |
files
|
Fri, 27 Sep 2013 09:07:45 +0200 |
Andreas Lochbihler |
add lemmas
|
changeset |
files
|
Fri, 27 Sep 2013 08:59:22 +0200 |
Andreas Lochbihler |
prefer Code.abort over code_abort
|
changeset |
files
|
Fri, 27 Sep 2013 09:17:25 +0200 |
lammich |
merged
|
changeset |
files
|
Thu, 26 Sep 2013 16:52:24 +0200 |
lammich |
Added Item_Net.retrieve_matching
|
changeset |
files
|
Thu, 26 Sep 2013 13:37:33 +0200 |
lammich |
Added symmetric code_unfold-lemmas for null and is_none
|
changeset |
files
|
Thu, 26 Sep 2013 16:33:34 -0700 |
huffman |
tuned proofs
|
changeset |
files
|
Thu, 26 Sep 2013 16:33:32 -0700 |
huffman |
moved lemma
|
changeset |
files
|