nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

QuotMain.thy

2009-10-12	Cezary Kaliszyk	Further with the manual proof	file \| diff \| annotate
2009-10-09	Cezary Kaliszyk	Further experiments with proving induction manually	file \| diff \| annotate
2009-10-09	Cezary Kaliszyk	Testing if I can prove the regularized version of induction manually	file \| diff \| annotate
2009-10-08	Christian Urban	exported parts of QuotMain into a separate ML-file	file \| diff \| annotate
2009-10-06	Christian Urban	consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar	file \| diff \| annotate
2009-10-06	Christian Urban	simplified typedef_quot_type_tac (using MetaSimplifier.rewrite_rule instead of the simplifier)	file \| diff \| annotate
2009-10-06	Christian Urban	renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)	file \| diff \| annotate
2009-10-06	Christian Urban	tuned; nothing serious	file \| diff \| annotate
2009-10-06	Christian Urban	another improvement to unlam_def	file \| diff \| annotate
2009-10-06	Christian Urban	one further improvement to unlam_def	file \| diff \| annotate
2009-10-05	Christian Urban	simplified the unlam_def function	file \| diff \| annotate
2009-10-05	Christian Urban	added an explicit syntax-argument to the function make_def (is needed if the user gives an syntax annotation for quotient types)	file \| diff \| annotate
2009-10-05	Christian Urban	used prop_of to get the term of a theorem (replaces crep_thm)	file \| diff \| annotate
2009-10-02	Cezary Kaliszyk	Merged	file \| diff \| annotate
2009-10-02	Cezary Kaliszyk	First theorem with quantifiers. Learned how to use sledgehammer.	file \| diff \| annotate
2009-10-01	Christian Urban	simplified the storage of the map-functions by using TheoryDataFun	file \| diff \| annotate
2009-09-30	Cezary Kaliszyk	Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.	file \| diff \| annotate
2009-09-29	Christian Urban	used new cong_tac	file \| diff \| annotate
2009-09-29	Cezary Kaliszyk	First version of handling of the universal quantifier	file \| diff \| annotate
2009-09-29	Cezary Kaliszyk	Handling abstraction correctly.	file \| diff \| annotate
2009-09-29	Cezary Kaliszyk	second test	file \| diff \| annotate
2009-09-29	Cezary Kaliszyk	Test line	file \| diff \| annotate
2009-09-29	Cezary Kaliszyk	Partially fix lifting of card_suc. The quantified variable still needs to be changed.	file \| diff \| annotate
2009-09-29	Cezary Kaliszyk	Tested new build_goal and removed old one, eq_reflection is included in atomize, card_suc tests.	file \| diff \| annotate
2009-09-29	Cezary Kaliszyk	Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.	file \| diff \| annotate
2009-09-29	Cezary Kaliszyk	Merged	file \| diff \| annotate
2009-09-28	Christian Urban	consistent state	file \| diff \| annotate
2009-09-28	Christian Urban	some tuning of my code	file \| diff \| annotate

less more (0) -50 -28 tip

nominal2

RSS Atom