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.
Quot/Examples/LamEx.thy
2010-01-24 Christian Urban test with splits file | diff | annotate
2010-01-23 Cezary Kaliszyk More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'. file | diff | annotate
2010-01-23 Cezary Kaliszyk Trying to define hom for the lifted type directly. file | diff | annotate
2010-01-20 Cezary Kaliszyk Statement of term1_hom_rsp file | diff | annotate
2010-01-20 Christian Urban proved that the function is a function file | diff | annotate
2010-01-20 Cezary Kaliszyk term1_hom as a function file | diff | annotate
2010-01-19 Cezary Kaliszyk A version of hom with quantifiers. file | diff | annotate
2010-01-16 Christian Urban fixed broken (partial) proof file | diff | annotate
2010-01-16 Christian Urban used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on file | diff | annotate
2010-01-16 Christian Urban liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals file | diff | annotate
2010-01-15 Christian Urban added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions file | diff | annotate
2010-01-15 Christian Urban tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely file | diff | annotate
2010-01-15 Cezary Kaliszyk hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize. file | diff | annotate
2010-01-15 Christian Urban slight tuning of relation_error file | diff | annotate
2010-01-15 Cezary Kaliszyk Appropriate respects and a statement of the lifted hom lemma file | diff | annotate
less more (0) -15 tip
nominal2