nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

Quot/QuotMain.thy

2009-12-08	Christian Urban	merged	file \| diff \| annotate
2009-12-08	Christian Urban	added preserve rules to the cleaning_tac	file \| diff \| annotate
2009-12-08	Cezary Kaliszyk	merge	file \| diff \| annotate
2009-12-08	Cezary Kaliszyk	cleaning.	file \| diff \| annotate
2009-12-08	Christian Urban	chnaged syntax to "lifting theorem"	file \| diff \| annotate
2009-12-08	Christian Urban	changed names of attributes	file \| diff \| annotate
2009-12-08	Christian Urban	merged	file \| diff \| annotate
2009-12-08	Christian Urban	added methods for the lifting_tac and the other tacs	file \| diff \| annotate
2009-12-08	Cezary Kaliszyk	make_inst3	file \| diff \| annotate
2009-12-08	Cezary Kaliszyk	trans2 replaced with equals_rsp_tac	file \| diff \| annotate
2009-12-08	Cezary Kaliszyk	Removed pattern from quot_rel_rsp, since list_rel and all used introduced ones cannot be patterned	file \| diff \| annotate
2009-12-08	Cezary Kaliszyk	Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.	file \| diff \| annotate
2009-12-08	Christian Urban	tuned	file \| diff \| annotate
2009-12-08	Christian Urban	the lift_tac produces a warning message if one of the three automatic proofs fails	file \| diff \| annotate
2009-12-08	Christian Urban	added a thm list for ids	file \| diff \| annotate
2009-12-08	Christian Urban	removed a fixme: map_info is now checked	file \| diff \| annotate
2009-12-07	Christian Urban	tuning of the code	file \| diff \| annotate
2009-12-07	Christian Urban	merged	file \| diff \| annotate
2009-12-07	Christian Urban	removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>	file \| diff \| annotate
2009-12-07	Cezary Kaliszyk	Handling of errors in lambda_prs_conv.	file \| diff \| annotate
2009-12-07	Christian Urban	clarified the function examples	file \| diff \| annotate
2009-12-07	Christian Urban	first attempt to deal with Babs in regularise and cleaning (not yet working)	file \| diff \| annotate
2009-12-07	Cezary Kaliszyk	make_inst for lambda_prs where the second quotient is not identity.	file \| diff \| annotate
2009-12-07	Cezary Kaliszyk	List moved after QuotMain	file \| diff \| annotate

less more (0) tip

nominal2

RSS Atom