nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

Quot/Examples/LamEx.thy

2010-01-15	Cezary Kaliszyk	Appropriate respects and a statement of the lifted hom lemma	file \| diff \| annotate
2010-01-15	Christian Urban	recursion-hom for lambda	file \| diff \| annotate
2010-01-15	Cezary Kaliszyk	Incorrect version of the homomorphism lemma	file \| diff \| annotate
2010-01-14	Christian Urban	tuned quotient_def.ML and cleaned somewhat LamEx.thy	file \| diff \| annotate
2010-01-14	Christian Urban	a few more lemmas...except supp of lambda-abstractions	file \| diff \| annotate
2010-01-14	Christian Urban	removed one sorry	file \| diff \| annotate
2010-01-14	Christian Urban	nearly all of the proof	file \| diff \| annotate
2010-01-14	Christian Urban	right generalisation	file \| diff \| annotate
2010-01-14	Cezary Kaliszyk	First subgoal.	file \| diff \| annotate
2010-01-14	Christian Urban	setup for strong induction	file \| diff \| annotate
2010-01-14	Cezary Kaliszyk	exported absrep_const for nitpick.	file \| diff \| annotate
2010-01-14	Cezary Kaliszyk	minor	file \| diff \| annotate
2010-01-01	Christian Urban	tuned	file \| diff \| annotate
2009-12-19	Christian Urban	on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file	file \| diff \| annotate
2009-12-19	Christian Urban	renamed "quotient" command to "quotient_type"; needs new keyword file to be installed	file \| diff \| annotate
2009-12-17	Christian Urban	moved the QuotMain code into two ML-files	file \| diff \| annotate
2009-12-11	Cezary Kaliszyk	New syntax for definitions.	file \| diff \| annotate
2009-12-09	Cezary Kaliszyk	Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.	file \| diff \| annotate
2009-12-08	Christian Urban	changed names of attributes	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	Christian Urban	added "end" to each example theory	file \| diff \| annotate
2009-12-07	Cezary Kaliszyk	List moved after QuotMain	file \| diff \| annotate
2009-12-07	Christian Urban	directory re-arrangement	file \| diff \| annotate \| base

less more (0) tip

nominal2

RSS Atom