nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

FSet.thy

2009-11-25	Cezary Kaliszyk	Moved exception handling to QuotMain and cleaned FSet.	file \| diff \| annotate
2009-11-25	Cezary Kaliszyk	Finished manual lifting of list_induct_part :)	file \| diff \| annotate
2009-11-25	Cezary Kaliszyk	Removed unused things from QuotMain.	file \| diff \| annotate
2009-11-25	Cezary Kaliszyk	lambda_prs and cleaning the existing examples.	file \| diff \| annotate
2009-11-25	Christian Urban	merged	file \| diff \| annotate
2009-11-25	Christian Urban	fixed the problem with generalising variables; at the moment it is quite a hack	file \| diff \| annotate
2009-11-24	Cezary Kaliszyk	Ho-matching failures...	file \| diff \| annotate
2009-11-24	Cezary Kaliszyk	Conversion	file \| diff \| annotate
2009-11-24	Cezary Kaliszyk	The non-working procedure_tac.	file \| diff \| annotate
2009-11-24	Cezary Kaliszyk	Fixes to the tactic after quotient_tac changed.	file \| diff \| annotate
2009-11-24	Cezary Kaliszyk	Another theorem for which the new regularize differs from old one, so the goal is not proved. But it seems, that the new one is better.	file \| diff \| annotate
2009-11-23	Christian Urban	fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)	file \| diff \| annotate
2009-11-23	Cezary Kaliszyk	Another not-typechecking regularized term.	file \| diff \| annotate
2009-11-23	Cezary Kaliszyk	domain_type in regularizing equality	file \| diff \| annotate
2009-11-23	Cezary Kaliszyk	More theorems lifted in the goal-directed way.	file \| diff \| annotate
2009-11-23	Cezary Kaliszyk	Move atomize_goal to QuotMain	file \| diff \| annotate
2009-11-23	Cezary Kaliszyk	Removed second implementation of Regularize/Inject from FSet.	file \| diff \| annotate
2009-11-23	Cezary Kaliszyk	New repabs behaves the same way as old one.	file \| diff \| annotate
2009-11-23	Christian Urban	code review with Cezary	file \| diff \| annotate
2009-11-23	Cezary Kaliszyk	The other branch does not seem to work...	file \| diff \| annotate
2009-11-23	Cezary Kaliszyk	Fixes for recent changes.	file \| diff \| annotate
2009-11-13	Cezary Kaliszyk	Still don't know how to do the proof automatically.	file \| diff \| annotate
2009-11-12	Cezary Kaliszyk	merged	file \| diff \| annotate
2009-11-11	Cezary Kaliszyk	Lifting towards goal and manually finished the proof.	file \| diff \| annotate

less more (0) -50 -24 tip

nominal2

RSS Atom