nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

Nominal/Ex/Let.thy

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
2011-06-20	Cezary Kaliszyk	Move lst_fcb to Nominal2_Abs	file \| diff \| annotate
2011-06-20	Cezary Kaliszyk	Let/minor	file \| diff \| annotate
2011-06-15	Cezary Kaliszyk	one TODO and one Problem?	file \| diff \| annotate
2011-06-10	Cezary Kaliszyk	Experiments with Let	file \| diff \| annotate
2011-02-07	Christian Urban	cleaned up the experiments so that the tests go through	file \| diff \| annotate
2011-02-04	Cezary Kaliszyk	Experiments defining a function on Let	file \| diff \| annotate
2011-01-18	Cezary Kaliszyk	alpha_abs_let_stronger is not true in the same form	file \| diff \| annotate
2010-12-28	Christian Urban	automated all strong induction lemmas	file \| diff \| annotate
2010-12-22	Christian Urban	corrected premises of strong exhausts theorems	file \| diff \| annotate
2010-12-22	Christian Urban	properly exported strong exhaust theorem; cleaned up some examples	file \| diff \| annotate
2010-11-13	Christian Urban	lifted permute_bn constants	file \| diff \| annotate
2010-11-13	Christian Urban	respectfulness for permute_bn functions	file \| diff \| annotate
2010-11-12	Christian Urban	automated permute_bn functions (raw ones first)	file \| diff \| annotate
2010-11-10	Christian Urban	adapted to changes by Florian on the quotient package and removed local fix for function package	file \| diff \| annotate
2010-10-06	Christian Urban	down to 21 pages and changed strong induction section	file \| diff \| annotate
2010-10-05	Christian Urban	llncs and more sqeezing	file \| diff \| annotate
2010-10-04	Christian Urban	changed to llncs	file \| diff \| annotate

less more (0) -30 tip

nominal2

RSS Atom