Mercurial Mercurial > hg > nominal2 / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -15 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Parser.thy
2010-03-16 Cezary Kaliszyk Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not. file | diff | annotate
2010-03-16 Cezary Kaliszyk FV_bn generated for recursive functions as well, and used in main fv for bindings. file | diff | annotate
2010-03-15 Cezary Kaliszyk fv_eqvt_cheat no longer needed. file | diff | annotate
2010-03-15 Cezary Kaliszyk derive "inducts" from "induct" instead of lifting again is much faster. file | diff | annotate
2010-03-15 Cezary Kaliszyk cheat_alpha_eqvt no longer needed; the proofs work. file | diff | annotate
2010-03-15 Cezary Kaliszyk explicit flag "cheat_equivp" file | diff | annotate
2010-03-13 Christian Urban started supp-fv proofs (is going to work) file | diff | annotate
2010-03-12 Cezary Kaliszyk Still don't know how to prove supp=fv for simplest Let... file | diff | annotate
2010-03-11 Cezary Kaliszyk Do not fail if the finite support proof fails. file | diff | annotate
2010-03-11 Christian Urban support of atoms at the end of Abs.thy file | diff | annotate
2010-03-11 Cezary Kaliszyk Show that the new types are in finite support typeclass. file | diff | annotate
2010-03-11 Cezary Kaliszyk Remove "_raw" from lifted theorems. file | diff | annotate
2010-03-11 Cezary Kaliszyk The cheats described explicitely. file | diff | annotate
2010-03-11 Cezary Kaliszyk With the 4 cheats, all examples fully lift. file | diff | annotate
2010-03-11 Cezary Kaliszyk Lift alpha_bn_constants. file | diff | annotate
less more (0) -15 tip
nominal2