Mercurial Mercurial > hg > nominal2 / shortlog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
 
2010-03-18 Cezary Kaliszyk Move most of the exporting out of the parser. changeset | files
2010-03-18 Cezary Kaliszyk Prove pseudo-inject (eq-iff) on the exported level and rename appropriately. changeset | files
2010-03-18 Cezary Kaliszyk Prove eqvts on exported terms. changeset | files
2010-03-18 Cezary Kaliszyk Clean 'Lift', start working only on exported things in Parser. changeset | files
2010-03-17 Christian Urban slightly more of the paper changeset | files
2010-03-17 Christian Urban merged changeset | files
2010-03-17 Christian Urban paper uses now a heap file - does not compile so long anymore changeset | files
2010-03-17 Cezary Kaliszyk merge changeset | files
2010-03-17 Cezary Kaliszyk compose_sym2 works also for term5 changeset | files
2010-03-17 Cezary Kaliszyk Updated Term1, including statement of strong induction. changeset | files
2010-03-17 Cezary Kaliszyk Proper compose_sym2 changeset | files
2010-03-17 Christian Urban merged changeset | files
2010-03-17 Christian Urban temporarily disabled tests in Nominal/ROOT changeset | files
2010-03-17 Christian Urban made paper to compile changeset | files
2010-03-17 Christian Urban added partial proof for the strong induction principle changeset | files
2010-03-17 Cezary Kaliszyk Trying to find a compose lemma for 2 arguments. changeset | files
2010-03-17 Cezary Kaliszyk merge changeset | files
2010-03-17 Cezary Kaliszyk cheat_alpha_eqvt no longer needed. Cleaned the tracing messages. changeset | files
2010-03-17 Christian Urban merged changeset | files
2010-03-17 Christian Urban added proof of supp/fv for type schemes changeset | files
2010-03-17 Cezary Kaliszyk Updated Type Schemes to automatic lifting. One goal is not true because of the restriction. changeset | files
2010-03-17 Cezary Kaliszyk Remove Term5a, since it is now identical to Term5. changeset | files
2010-03-17 Cezary Kaliszyk merge changeset | files
2010-03-17 Cezary Kaliszyk Finished all proofs in Term5 and Term5n. changeset | files
2010-03-17 Christian Urban added partial proof of supp for type schemes changeset | files
2010-03-17 Cezary Kaliszyk Fix in alpha; support of the recursive Let works :) changeset | files
2010-03-17 Cezary Kaliszyk The recursive supp just has one equation too much. changeset | files
2010-03-17 Cezary Kaliszyk Fix for the change of alpha_gen. changeset | files
2010-03-17 Cezary Kaliszyk merge changeset | files
2010-03-17 Cezary Kaliszyk Generate compound FV and Alpha for recursive bindings. changeset | files
(0) -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 tip
nominal2