| Sun, 22 Aug 2010 11:00:53 +0800 | Christian Urban | updated to new Isabelle | file | diff | annotate |
| Wed, 11 Aug 2010 16:23:50 +0800 | Christian Urban | updated to Isabelle 11 Aug | file | diff | annotate |
| Thu, 24 Jun 2010 19:32:33 +0100 | Christian Urban | fixed according to changes in quotient | file | diff | annotate |
| 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 |