Mercurial Mercurial > hg > nominal2 / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -50 -24 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/Nominal/Terms.thy
2010-02-19 Cezary Kaliszyk Constructing alpha_inj goal. file | diff | annotate
2010-02-18 Christian Urban merged file | diff | annotate
2010-02-18 Cezary Kaliszyk Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct. file | diff | annotate
2010-02-18 Cezary Kaliszyk Testing auto constant lifting. file | diff | annotate
2010-02-18 Cezary Kaliszyk Changed back to original version of trm5 file | diff | annotate
2010-02-18 Cezary Kaliszyk The alternate version of trm5 with additional binding. All proofs work the same. file | diff | annotate
2010-02-18 Cezary Kaliszyk Code for handling atom sets. file | diff | annotate
2010-02-18 Cezary Kaliszyk Replace Terms by Terms2. file | diff | annotate | base
2010-02-18 Cezary Kaliszyk Fixed proofs in Terms2 and found a mistake in Terms. file | diff | annotate
2010-02-17 Cezary Kaliszyk Cleaning of proofs in Terms. file | diff | annotate
2010-02-17 Cezary Kaliszyk Testing Fv file | diff | annotate
2010-02-17 Cezary Kaliszyk Fix the strong induction principle. file | diff | annotate
2010-02-17 Cezary Kaliszyk Tested the Perm code; works everywhere in Terms. file | diff | annotate
2010-02-12 Cezary Kaliszyk renamed 'as' to 'is' everywhere. file | diff | annotate
2010-02-11 Cezary Kaliszyk the lam/bla example. file | diff | annotate
2010-02-11 Cezary Kaliszyk Finished a working foo/bar. file | diff | annotate
2010-02-11 Cezary Kaliszyk fv_foo is not regular. file | diff | annotate
2010-02-11 Cezary Kaliszyk Testing foo/bar file | diff | annotate
2010-02-11 Cezary Kaliszyk Even when bv = fv it still doesn't lift. file | diff | annotate
2010-02-11 Cezary Kaliszyk Notation available locally file | diff | annotate
2010-02-11 Cezary Kaliszyk Main renaming + fixes for new Isabelle in IntEx2. file | diff | annotate
2010-02-10 Cezary Kaliszyk example with a respectful bn function defined over the type itself file | diff | annotate
2010-02-10 Cezary Kaliszyk Another mistake found with OTT. file | diff | annotate
2010-02-10 Cezary Kaliszyk Fixed rbv6, when translating to OTT. file | diff | annotate
less more (0) -50 -24 tip
nominal2