nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

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

QuotMain.thy

2009-09-28	Christian Urban	added ctxt as explicit argument to build_goal; tuned	file \| diff \| annotate
2009-09-25	Christian Urban	slightly tuned the comment for unlam	file \| diff \| annotate
2009-09-25	Christian Urban	fixed a bug in my code: function typedef_term constructs now now the correct term when the relation is called x	file \| diff \| annotate
2009-09-25	Christian Urban	tuned slightly one proof	file \| diff \| annotate
2009-09-25	Cezary Kaliszyk	A version of the tactic that exports variables correctly.	file \| diff \| annotate
2009-09-25	Cezary Kaliszyk	Minor cleaning: whitespace, commas etc.	file \| diff \| annotate
2009-09-24	Cezary Kaliszyk	Correctly handling abstractions while building goals	file \| diff \| annotate
2009-09-24	Cezary Kaliszyk	Minor cleanup	file \| diff \| annotate
2009-09-24	Cezary Kaliszyk	Found the source for the exception and added a handle for it.	file \| diff \| annotate
2009-09-24	Cezary Kaliszyk	Make the tactic use Trueprop_cong and atomize.	file \| diff \| annotate
2009-09-23	Cezary Kaliszyk	Proper code for getting the prop out of the theorem.	file \| diff \| annotate
2009-09-23	Cezary Kaliszyk	Using "atomize" the versions with arbitrary Trueprops can be proven.	file \| diff \| annotate
2009-09-22	Cezary Kaliszyk	Proper definition of CARD and some properties of it.	file \| diff \| annotate
2009-09-22	Christian Urban	some comments	file \| diff \| annotate
2009-09-21	Christian Urban	merged	file \| diff \| annotate
2009-09-21	Christian Urban	slight tuning	file \| diff \| annotate

less more (0) -16 tip

nominal2