Mercurial Mercurial > hg > nominal2 / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -24 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Parser.thy
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
2010-03-11 Cezary Kaliszyk Lifting constants. file | diff | annotate
2010-03-11 Cezary Kaliszyk Lifting constants works for all examples. file | diff | annotate
2010-03-11 Cezary Kaliszyk Equivp working only on the standard alpha-equivalences. file | diff | annotate
2010-03-11 Cezary Kaliszyk explicit cheat_fv_eqvt file | diff | annotate
2010-03-11 Cezary Kaliszyk extract build_eqvts_tac. file | diff | annotate
2010-03-11 Cezary Kaliszyk build_eqvts no longer requires permutations. file | diff | annotate
2010-03-11 Cezary Kaliszyk Add explicit alpha_eqvt_cheat. file | diff | annotate
2010-03-11 Cezary Kaliszyk Export tactic out of alpha_eqvt. file | diff | annotate
2010-03-10 Christian Urban merged file | diff | annotate
2010-03-10 Christian Urban almost done with showing the equivalence between old and new alpha-equivalence (one subgoal remaining) file | diff | annotate
2010-03-10 Cezary Kaliszyk Undoing mistakenly committed parser experiments. file | diff | annotate
2010-03-10 Cezary Kaliszyk alpha_eqvt for recursive term1. file | diff | annotate
2010-03-10 Cezary Kaliszyk Linked parser to fv and alpha. file | diff | annotate
2010-03-10 Christian Urban parser produces ordered bn-fun information file | diff | annotate
2010-03-09 Christian Urban added bn-information, but it is not yet ordered according to the dts file | diff | annotate
2010-03-09 Cezary Kaliszyk A version of Fv that takes into account recursive and non-recursive bindings. file | diff | annotate
2010-03-08 Christian Urban merged file | diff | annotate
2010-03-08 Christian Urban updated to new Isabelle file | diff | annotate
2010-03-08 Cezary Kaliszyk More fine-grained nominal restriction for debugging. file | diff | annotate
2010-03-05 Cezary Kaliszyk Lift fv and bn eqvts; no need to lift alpha_eqvt. file | diff | annotate
less more (0) -24 tip
nominal2