nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

LamEx.thy

2009-12-04	Cezary Kaliszyk	Fixes after big merge.	file \| diff \| annotate
2009-12-04	Cezary Kaliszyk	The big merge; probably non-functional.	file \| diff \| annotate
2009-12-04	Cezary Kaliszyk	Testing the new tactic everywhere	file \| diff \| annotate
2009-12-04	Cezary Kaliszyk	Even better: Completely got rid of the simps in both quotient_tac and inj_repabs_tac	file \| diff \| annotate
2009-12-04	Cezary Kaliszyk	Made your version work again with LIST_REL_EQ.	file \| diff \| annotate
2009-12-03	Cezary Kaliszyk	Reintroduced varifyT; we still need it for permutation definition.	file \| diff \| annotate
2009-12-03	Cezary Kaliszyk	Updated the examples	file \| diff \| annotate
2009-12-02	Cezary Kaliszyk	Experiments with OPTION_map	file \| diff \| annotate
2009-11-30	Cezary Kaliszyk	Code cleaning.	file \| diff \| annotate
2009-11-29	Cezary Kaliszyk	Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.	file \| diff \| annotate
2009-11-28	Christian Urban	renamed r_mk_comb_tac to inj_repabs_tac	file \| diff \| annotate
2009-11-27	Cezary Kaliszyk	Simplifying arguments; got rid of trans2_thm.	file \| diff \| annotate
2009-11-27	Cezary Kaliszyk	Recommit	file \| diff \| annotate
2009-11-27	Cezary Kaliszyk	Removing arguments of tactics: absrep, rel_refl, reps_same are computed.	file \| diff \| annotate
2009-11-25	Cezary Kaliszyk	applic_prs	file \| diff \| annotate
2009-11-25	Cezary Kaliszyk	Removed unused things from QuotMain.	file \| diff \| annotate
2009-11-25	Cezary Kaliszyk	All examples work again.	file \| diff \| annotate
2009-11-25	Cezary Kaliszyk	lambda_prs and cleaning the existing examples.	file \| diff \| annotate
2009-11-24	Cezary Kaliszyk	Lambda & SOLVED' for new quotient_tac	file \| diff \| annotate
2009-11-05	Cezary Kaliszyk	More functionality for lifting list.cases and list.recs.	file \| diff \| annotate
2009-11-05	Christian Urban	merged	file \| diff \| annotate
2009-11-05	Cezary Kaliszyk	Infrastructure for polymorphic types	file \| diff \| annotate
2009-11-04	Cezary Kaliszyk	Lifting 'fold1.simps(2)' and some cleaning.	file \| diff \| annotate
2009-11-03	Cezary Kaliszyk	Playing with alpha_refl.	file \| diff \| annotate
2009-11-03	Cezary Kaliszyk	Alpha.induct now lifts automatically.	file \| diff \| annotate
2009-11-03	Cezary Kaliszyk	merge	file \| diff \| annotate
2009-11-03	Cezary Kaliszyk	applic_prs	file \| diff \| annotate
2009-11-03	Christian Urban	simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated	file \| diff \| annotate
2009-11-03	Cezary Kaliszyk	Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP	file \| diff \| annotate
2009-11-03	Cezary Kaliszyk	Preparing infrastructure for general FORALL_PRS	file \| diff \| annotate

less more (0) -50 -30 tip

nominal2

RSS Atom