| Thu, 06 Mar 2014 14:57:14 +0100 |
blanchet |
renamed 'set_rel' to 'rel_set'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 13:36:49 +0100 |
blanchet |
renamed 'fset_rel' to 'rel_fset'
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 19:07:42 +0100 |
kuncar |
simplify a proof due to 6c95a39348bd
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 15:02:20 +0100 |
kuncar |
simplify and repair proofs due to df0fda378813
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 23:03:50 +0100 |
kuncar |
simplify proofs because of the stronger reflexivity prover
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Fri, 24 Jan 2014 11:51:45 +0100 |
blanchet |
killed 'More_BNFs' by moving its various bits where they (now) belong
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:44:58 +0100 |
hoelzl |
use bdd_above and bdd_below for conditionally complete lattices
|
file |
diff |
annotate
|
| Tue, 01 Oct 2013 17:06:35 +0200 |
traytel |
base the fset bnf on the new FSet theory
|
file |
diff |
annotate
|
| Sat, 28 Sep 2013 14:41:46 +0200 |
wenzelm |
proper document markup;
|
file |
diff |
annotate
|
| Fri, 27 Sep 2013 21:54:55 +0200 |
kuncar |
tuned names
|
file |
diff |
annotate
|
| Fri, 27 Sep 2013 21:54:55 +0200 |
kuncar |
fold and lemmas about cardinality
|
file |
diff |
annotate
|
| Fri, 27 Sep 2013 14:43:26 +0200 |
kuncar |
new theory of finite sets as a subtype
|
file |
diff |
annotate
|