nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -15 tip

Nominal/Ex/Let.thy

2012-06-04	Christian Urban	added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often	file \| diff \| annotate
2011-12-17	Christian Urban	cleaned examples for stable branch Nominal2-Isabelle2011-1	file \| diff \| annotate
2011-07-17	Christian Urban	some tuning	file \| diff \| annotate
2011-07-06	Christian Urban	more on NBE	file \| diff \| annotate
2011-07-05	Christian Urban	changed bind to binds in specifications; bind will cause trouble with Monad_Syntax	file \| diff \| annotate
2011-07-05	Christian Urban	exported various FCB-lemmas to a separate file	file \| diff \| annotate
2011-07-04	Christian Urban	tuned	file \| diff \| annotate
2011-07-02	Cezary Kaliszyk	Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn	file \| diff \| annotate
2011-07-01	Christian Urban	side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function	file \| diff \| annotate
2011-06-29	Christian Urban	moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through	file \| diff \| annotate
2011-06-29	Christian Urban	added a warning if a theorem is already declared as equivariant	file \| diff \| annotate
2011-06-29	Christian Urban	merged	file \| diff \| annotate
2011-06-29	Cezary Kaliszyk	Prove bn injectivity and experiment more with Let	file \| diff \| annotate
2011-06-28	Christian Urban	some experiments	file \| diff \| annotate
2011-06-28	Cezary Kaliszyk	trying new fcb in let/subst	file \| diff \| annotate

less more (0) -15 tip

nominal2