Mercurial Mercurial > hg > nominal2 / shortlog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -1000 -300 -100 -50 -32 +32 +50 +100 +300 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
 
2011-06-01 Cezary Kaliszyk proved subst for All constructor in type schemes. changeset | files
2011-06-01 Cezary Kaliszyk DB translation using index; easier to reason about. changeset | files
2011-06-01 Cezary Kaliszyk Problem: free variables in the goal changeset | files
2011-06-01 Cezary Kaliszyk fixed previous commit changeset | files
2011-06-01 Cezary Kaliszyk equivariance of db_trans changeset | files
2011-05-31 Christian Urban fixed the problem with cps-like functions changeset | files
2011-05-31 Cezary Kaliszyk DeBruijn translation in a simplifier friendly way changeset | files
2011-05-31 Cezary Kaliszyk map_term can be defined when equivariance is assumed changeset | files
2011-05-31 Cezary Kaliszyk map_term is not a function the way it is defined changeset | files
2011-05-31 Cezary Kaliszyk Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case. changeset | files
2011-05-31 Cezary Kaliszyk Simple eqvt proofs with perm_simps for clarity changeset | files
2011-05-30 Christian Urban tuned last commit changeset | files
2011-05-30 Christian Urban functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition changeset | files
2011-05-26 Christian Urban updated to new Isabelle changeset | files
2011-05-25 Christian Urban added eq_iff and distinct lemmas of nominal datatypes to the simplifier changeset | files
2011-05-24 Christian Urban more on slides changeset | files
2011-05-22 Christian Urban added slides for copenhagen changeset | files
2011-05-14 Christian Urban added a problem with inductive_cases (reported by Randy) changeset | files
2011-05-13 Christian Urban misc changeset | files
2011-05-10 Christian Urban made the subtyping work again changeset | files
2011-05-10 Christian Urban updated to new Isabelle (> 9 May) changeset | files
2011-05-09 Christian Urban merged changeset | files
2011-05-03 Christian Urban added two mutual recursive inductive definitions changeset | files
2011-05-03 Christian Urban deleted two functions from the API changeset | files
2011-05-03 Christian Urban proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates) changeset | files
2011-05-09 Christian Urban more on pearl-paper changeset | files
2011-05-04 Christian Urban more on pearl-paper changeset | files
2011-05-02 Christian Urban updated Quotient paper so that it compiles again changeset | files
2011-04-28 Christian Urban merged changeset | files
2011-04-28 Christian Urban added slides for beijing changeset | files
2011-04-21 Christian Urban more to the pearl paper changeset | files
2011-04-19 Christian Urban updated to snapshot Isabelle 19 April changeset | files
(0) -1000 -300 -100 -50 -32 +32 +50 +100 +300 tip
nominal2