| Wed, 03 Feb 2010 12:44:29 +0100 | Christian Urban | fixed proofs that broke because of eqvt | changeset | files |
| Wed, 03 Feb 2010 12:34:53 +0100 | Cezary Kaliszyk | Minor fix. | changeset | files |
| Wed, 03 Feb 2010 12:34:01 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Wed, 03 Feb 2010 12:29:45 +0100 | Cezary Kaliszyk | alpha5 pseudo-injective | changeset | files |
| Wed, 03 Feb 2010 12:31:58 +0100 | Christian Urban | fixed proofs in Abs.thy | changeset | files |
| Wed, 03 Feb 2010 12:13:22 +0100 | Christian Urban | merged | changeset | files |
| Wed, 03 Feb 2010 12:06:10 +0100 | Christian Urban | added a first eqvt_tac which pushes permutations inside terms | changeset | files |
| Wed, 03 Feb 2010 12:11:23 +0100 | Cezary Kaliszyk | The alpha-equivalence relation for let-rec. Not sure if correct... | changeset | files |
| Wed, 03 Feb 2010 11:47:37 +0100 | Cezary Kaliszyk | Starting with a let-rec example. | changeset | files |
| Wed, 03 Feb 2010 11:21:34 +0100 | Cezary Kaliszyk | Minor | changeset | files |
| Wed, 03 Feb 2010 10:50:24 +0100 | Cezary Kaliszyk | Some cleaning and eqvt proof | changeset | files |
| Wed, 03 Feb 2010 09:25:21 +0100 | Cezary Kaliszyk | The trm1_support lemma explicitly and stated a strong induction principle. | changeset | files |
| Wed, 03 Feb 2010 08:32:24 +0100 | Cezary Kaliszyk | More ingredients in Terms. | changeset | files |
| Tue, 02 Feb 2010 17:10:42 +0100 | Cezary Kaliszyk | Finished the supp_fv proof; first proof that analyses the structure of 'Let' :) | changeset | files |