| Thu, 27 May 2010 18:30:26 +0200 |
Christian Urban |
fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set
|
file |
diff |
annotate
|
| Fri, 14 May 2010 15:37:23 +0200 |
Cezary Kaliszyk |
Proper fv/alpha for multiple compound binders
|
file |
diff |
annotate
|
| Wed, 12 May 2010 16:08:32 +0200 |
Cezary Kaliszyk |
Use raw_induct instead of induct
|
file |
diff |
annotate
|
| Mon, 10 May 2010 15:09:32 +0200 |
Cezary Kaliszyk |
Use mk_compound_fv' and mk_compound_rel'
|
file |
diff |
annotate
|
| Thu, 06 May 2010 14:13:35 +0200 |
Cezary Kaliszyk |
Fixes for new Isabelle
|
file |
diff |
annotate
|
| Thu, 06 May 2010 14:13:05 +0200 |
Cezary Kaliszyk |
compound versions with prod_rel and prod_fun, not made default yet.
|
file |
diff |
annotate
|
| Sun, 02 May 2010 16:01:45 +0100 |
Christian Urban |
replaced make_pair with library function HOLogic.mk_prod
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 10:31:32 +0200 |
Cezary Kaliszyk |
Change signature of fv and alpha generation.
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 17:52:19 +0200 |
Cezary Kaliszyk |
New Alpha.
|
file |
diff |
annotate
|