nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

QuotMain.thy

2009-10-19	Christian Urban	my version of regularise (still needs to be completed)	file \| diff \| annotate
2009-10-19	Christian Urban	moved the map-info and fun-info section to quotient.ML	file \| diff \| annotate
2009-10-18	Cezary Kaliszyk	Test if we can already do sth with the transformed theorem.	file \| diff \| annotate
2009-10-18	Christian Urban	slight fix and tuning	file \| diff \| annotate
2009-10-17	Christian Urban	the command "quotient" can now define more than one quotient at the same time; quotients need to be separated by and	file \| diff \| annotate
2009-10-17	Cezary Kaliszyk	Partial simplification of the proof	file \| diff \| annotate
2009-10-17	Cezary Kaliszyk	Some QUOTIENTS	file \| diff \| annotate
2009-10-17	Cezary Kaliszyk	Only QUOTIENSs are left to fnish proof	file \| diff \| annotate
2009-10-17	Cezary Kaliszyk	More higher order unification problems	file \| diff \| annotate
2009-10-17	Cezary Kaliszyk	Merged	file \| diff \| annotate
2009-10-17	Cezary Kaliszyk	Simplified	file \| diff \| annotate
2009-10-17	Cezary Kaliszyk	Further in the proof	file \| diff \| annotate
2009-10-17	Cezary Kaliszyk	compose_tac works with the full instantiation.	file \| diff \| annotate
2009-10-17	Christian Urban	slightly simplified get_fun function	file \| diff \| annotate
2009-10-17	Cezary Kaliszyk	The instantiated version is the same modulo beta	file \| diff \| annotate
2009-10-17	Cezary Kaliszyk	Fully manually instantiated. Still fails...	file \| diff \| annotate
2009-10-17	Cezary Kaliszyk	Little progress with match/instantiate	file \| diff \| annotate
2009-10-16	Cezary Kaliszyk	Fighting with the instantiation	file \| diff \| annotate
2009-10-16	Cezary Kaliszyk	Symmetric version of REP_ABS_RSP	file \| diff \| annotate
2009-10-16	Cezary Kaliszyk	Progressing with the proof	file \| diff \| annotate
2009-10-16	Cezary Kaliszyk	Finally fix get_fun.	file \| diff \| annotate
2009-10-16	Cezary Kaliszyk	A fix for one fun_map; doesn't work for more.	file \| diff \| annotate
2009-10-16	Christian Urban	fixed the problem with function types; but only type_of works; cterm_of does not work	file \| diff \| annotate
2009-10-15	Cezary Kaliszyk	Description of the problem with get_fun.	file \| diff \| annotate
2009-10-15	Cezary Kaliszyk	A proper build_goal_term function.	file \| diff \| annotate
2009-10-15	Cezary Kaliszyk	Cleaning the code	file \| diff \| annotate
2009-10-15	Cezary Kaliszyk	Merged	file \| diff \| annotate
2009-10-15	Cezary Kaliszyk	Cleaning the proofs	file \| diff \| annotate

less more (0) -100 -50 -28 tip

nominal2

RSS Atom