nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

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

LFex.thy

2009-11-28	Cezary Kaliszyk	Finished and tested the new regularize	file \| diff \| annotate
2009-11-28	Cezary Kaliszyk	Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.	file \| diff \| annotate
2009-11-28	Cezary Kaliszyk	Integrated Stefan's tactic and changed substs to simps with empty context.	file \| diff \| annotate
2009-11-27	Cezary Kaliszyk	The magical code from Stefan, will need to be integrated in the Simproc.	file \| diff \| annotate
2009-11-27	Cezary Kaliszyk	Simplifying arguments; got rid of trans2_thm.	file \| diff \| annotate
2009-11-27	Cezary Kaliszyk	Cleaning of LFex. Lambda_prs fails to unify in 2 places.	file \| diff \| annotate
2009-11-27	Cezary Kaliszyk	Removing arguments of tactics: absrep, rel_refl, reps_same are computed.	file \| diff \| annotate
2009-11-27	Cezary Kaliszyk	Minor cleaning	file \| diff \| annotate
2009-11-26	Cezary Kaliszyk	Merged	file \| diff \| annotate
2009-11-26	Christian Urban	introduced a new property for Ball and ===> on the left	file \| diff \| annotate
2009-11-26	Cezary Kaliszyk	Manually regularized akind_aty_atrm.induct	file \| diff \| annotate
2009-11-26	Cezary Kaliszyk	Playing with Monos in LFex.	file \| diff \| annotate
2009-11-09	Cezary Kaliszyk	Cleaning and commenting	file \| diff \| annotate
2009-11-06	Christian Urban	permutation lifting works now also	file \| diff \| annotate
2009-11-06	Christian Urban	updated to new Isabelle version and added a new example file	file \| diff \| annotate

less more (0) tip

nominal2