nominal2: File revisions

Quot/Examples/IntEx2.thy

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-11	Cezary Kaliszyk	Renaming	file \| diff \| annotate
2009-12-11	Christian Urban	added Int example from Larry	file \| diff \| annotate
2009-12-11	Cezary Kaliszyk	More theorem renaming.	file \| diff \| annotate
2009-12-11	Cezary Kaliszyk	Renamed theorems in IntEx2 to conform to names in Int.	file \| diff \| annotate
2009-12-11	Cezary Kaliszyk	New syntax for definitions.	file \| diff \| annotate
2009-12-10	Cezary Kaliszyk	Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.	file \| diff \| annotate
2009-12-10	Cezary Kaliszyk	Removed 'Presburger' as it introduces int & other minor cleaning in Int2.	file \| diff \| annotate
2009-12-10	Christian Urban	merged	file \| diff \| annotate
2009-12-10	Cezary Kaliszyk	With int_of_nat as a quotient_def, lemmas about it can be easily lifted.	file \| diff \| annotate
2009-12-10	Christian Urban	merged	file \| diff \| annotate
2009-12-10	Christian Urban	naming in this file cannot be made to agree to the original (PROBLEM?)	file \| diff \| annotate
2009-12-10	Cezary Kaliszyk	Lifted some kind of induction.	file \| diff \| annotate
2009-12-09	Christian Urban	more proofs in IntEx2	file \| diff \| annotate

nominal2