| Mon, 26 Oct 2009 11:34:02 +0100 | Cezary Kaliszyk | Making all the definitions from the original ones | file | diff | annotate |
| Mon, 26 Oct 2009 10:02:50 +0100 | Cezary Kaliszyk | Cleaning and fixing. | file | diff | annotate |
| Sun, 25 Oct 2009 01:15:03 +0200 | Christian Urban | proved the two lemmas in QuotScript (reformulated them without leading forall) | file | diff | annotate |
| Sat, 24 Oct 2009 18:17:38 +0200 | Christian Urban | changed the definitions of liftet constants to use fun_maps | file | diff | annotate |
| Sat, 24 Oct 2009 17:29:27 +0200 | Cezary Kaliszyk | Finally lifted induction, with some manually added simplification lemmas. | file | diff | annotate |
| Sat, 24 Oct 2009 16:15:33 +0200 | cek | Merge | file | diff | annotate |
| Sat, 24 Oct 2009 16:15:58 +0200 | Cezary Kaliszyk | Preparing infrastructire for LAMBDA_PRS | file | diff | annotate |
| Sat, 24 Oct 2009 16:09:05 +0200 | Christian Urban | moved the map_funs setup into QuotMain | file | diff | annotate |