nominal2: File revisions

QuotMain.thy

2009-11-04	Christian Urban	separated the quotient_def into a separate file	file \| diff \| annotate
2009-11-04	Christian Urban	fixed definition of PLUS	file \| diff \| annotate
2009-11-04	Christian Urban	simplified the quotient_def code	file \| diff \| annotate
2009-11-04	Cezary Kaliszyk	Lifting 'fold1.simps(2)' and some cleaning.	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-02	Christian Urban	split quotient.ML into two files	file \| diff \| annotate
2009-11-02	Christian Urban	slightly saner way of parsing the quotient_def	file \| diff \| annotate
2009-11-02	Christian Urban	changed Type.typ_match to Sign.typ_match	file \| diff \| annotate
2009-11-02	Cezary Kaliszyk	Optimization	file \| diff \| annotate
2009-11-02	Cezary Kaliszyk	Fixed quotdata_lookup.	file \| diff \| annotate
2009-11-02	Christian Urban	merged	file \| diff \| annotate
2009-11-02	Christian Urban	fixed the problem with types in map	file \| diff \| annotate

nominal2