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

Quot/Examples/FSet.thy

2010-02-12	Cezary Kaliszyk	merge	file \| diff \| annotate
2010-02-12	Cezary Kaliszyk	renamed 'as' to 'is' everywhere.	file \| diff \| annotate
2010-02-12	Christian Urban	moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned	file \| diff \| annotate
2010-02-11	Cezary Kaliszyk	Main renaming + fixes for new Isabelle in IntEx2.	file \| diff \| annotate
2010-01-26	Cezary Kaliszyk	2 cases for regularize with split, lemmas with split now lift.	file \| diff \| annotate
2010-01-26	Cezary Kaliszyk	Simpler statement that has the problem.	file \| diff \| annotate
2010-01-26	Cezary Kaliszyk	Found a term that does not regularize.	file \| diff \| annotate
2010-01-26	Cezary Kaliszyk	A triple is still ok.	file \| diff \| annotate
2010-01-26	Cezary Kaliszyk	Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work.	file \| diff \| annotate
2010-01-26	Cezary Kaliszyk	Generalized split_prs and split_rsp	file \| diff \| annotate
2010-01-24	Christian Urban	test with splits	file \| diff \| annotate
2009-12-24	Christian Urban	made the quotient_type definition more like typedef; now type variables need to be explicitly given	file \| diff \| annotate
2009-12-23	Christian Urban	corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file	file \| diff \| annotate
2009-12-22	Christian Urban	renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions	file \| diff \| annotate
2009-12-22	Christian Urban	moved get_fun into quotient_term; this simplifies the overall including structure of the package	file \| diff \| annotate

less more (0) -15 tip

nominal2