| Mon, 17 May 2010 17:31:18 +0200 |
Cezary Kaliszyk |
alpha_alphabn for bindings in a type under bn.
|
file |
diff |
annotate
|
| Wed, 12 May 2010 16:57:01 +0200 |
Cezary Kaliszyk |
include set_simps and append_simps in fv_rsp
|
file |
diff |
annotate
|
| Wed, 12 May 2010 16:39:10 +0200 |
Cezary Kaliszyk |
Move alpha_eqvt to unused.
|
file |
diff |
annotate
|
| Wed, 12 May 2010 16:11:23 +0200 |
Cezary Kaliszyk |
merge
|
file |
diff |
annotate
|
| Wed, 12 May 2010 16:11:03 +0200 |
Cezary Kaliszyk |
fvbv_rsp include prod_rel.simps
|
file |
diff |
annotate
|
| Wed, 12 May 2010 16:08:32 +0200 |
Cezary Kaliszyk |
Use raw_induct instead of induct
|
file |
diff |
annotate
|
| Thu, 06 May 2010 14:21:10 +0200 |
Cezary Kaliszyk |
alpha_eqvt_tac with prod_rel and prod_fv simps
|
file |
diff |
annotate
|
| Thu, 06 May 2010 14:10:56 +0200 |
Cezary Kaliszyk |
prod_rel and prod_fv simps
|
file |
diff |
annotate
|
| Mon, 03 May 2010 15:37:21 +0200 |
Cezary Kaliszyk |
alpha_eqvt_tac fixed to work when the existential is not at the top level.
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 17:26:07 +0200 |
Christian Urban |
deleting function perm_arg in favour of the library function mk_perm
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 10:35:08 +0200 |
Cezary Kaliszyk |
Accept non-equality eqvt rules in support proofs.
|
file |
diff |
annotate
|
| Thu, 01 Apr 2010 08:48:33 +0200 |
Cezary Kaliszyk |
Let with multiple bindings.
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 14:55:07 +0100 |
Cezary Kaliszyk |
Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 13:50:59 +0100 |
Cezary Kaliszyk |
Get lifted types information from the quotient package.
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 08:42:07 +0100 |
Cezary Kaliszyk |
New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
|
file |
diff |
annotate
|