| Wed, 19 Mar 2014 18:47:22 +0100 |
haftmann |
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 22:11:46 +0100 |
haftmann |
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
|
file |
diff |
annotate
|
| Sun, 16 Mar 2014 18:09:04 +0100 |
haftmann |
normalising simp rules for compound operators
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 14:57:14 +0100 |
blanchet |
renamed 'set_rel' to 'rel_set'
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 23:03:49 +0100 |
kuncar |
delete or move now not necessary reflexivity rules due to 1726f46d2aa8
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:44:57 +0100 |
hoelzl |
generalize SUP and INF to the syntactic type classes Sup and Inf
|
file |
diff |
annotate
|
| Fri, 27 Sep 2013 14:43:26 +0200 |
kuncar |
new parametricity rules and useful lemmas
|
file |
diff |
annotate
|
| Fri, 27 Sep 2013 09:15:40 +0200 |
Andreas Lochbihler |
tuned proofs
|
file |
diff |
annotate
|
| Thu, 26 Sep 2013 15:50:33 +0200 |
Andreas Lochbihler |
add lemmas
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 15:59:22 +0200 |
kuncar |
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
|
file |
diff |
annotate
|