isabelle: File revisions

src/HOL/Library/Quotient.thy

2007-03-20	haftmann	2007-03-20	explizit "type" superclass	file \| diff \| annotate
2007-03-02	haftmann	2007-03-02	now using "class"	file \| diff \| annotate
2006-11-17	wenzelm	2006-11-17	more robust syntax for definition/abbreviation/notation;	file \| diff \| annotate
2006-02-16	wenzelm	2006-02-16	new-style definitions/abbreviations;	file \| diff \| annotate
2006-01-21	wenzelm	2006-01-21	tuned proofs;	file \| diff \| annotate
2006-01-03	haftmann	2006-01-03	class now an keyword, quoted where necessary	file \| diff \| annotate
2005-12-08	wenzelm	2005-12-08	tuned proofs;	file \| diff \| annotate
2004-08-18	nipkow	2004-08-18	import -> imports	file \| diff \| annotate
2004-08-16	nipkow	2004-08-16	New theory header syntax.	file \| diff \| annotate
2004-06-21	kleing	2004-06-21	Merged in license change from Isabelle2004	file \| diff \| annotate
2004-05-06	wenzelm	2004-05-06	tuned document;	file \| diff \| annotate
2001-12-05	wenzelm	2001-12-05	tuned;	file \| diff \| annotate
2001-12-01	wenzelm	2001-12-01	renamed class "term" to "type" (actually "HOL.type");	file \| diff \| annotate
2001-09-04	wenzelm	2001-09-04	renamed "antecedent" case to "rule_context";	file \| diff \| annotate
2001-02-12	wenzelm	2001-02-12	\<subseteq>;	file \| diff \| annotate
2000-12-15	wenzelm	2000-12-15	GPLed;	file \| diff \| annotate
2000-11-30	wenzelm	2000-11-30	renamed "equivalence_class" to "class";	file \| diff \| annotate
2000-11-21	wenzelm	2000-11-21	unsymbolize;	file \| diff \| annotate
2000-11-21	bauerg	2000-11-21	alternative function definition;	file \| diff \| annotate
2000-11-18	wenzelm	2000-11-18	quot_cond_function: simplified, support conditional definition;	file \| diff \| annotate
2000-11-17	wenzelm	2000-11-17	removed quot_cond_function1, quot_function1; removed overloaded standard operations;	file \| diff \| annotate
2000-11-16	wenzelm	2000-11-16	added not_equiv_sym, not_equiv_trans1/2; tuned;	file \| diff \| annotate
2000-11-15	wenzelm	2000-11-15	separate rules for function/operation definitions;	file \| diff \| annotate
2000-11-12	wenzelm	2000-11-12	quot_cond_definition;	file \| diff \| annotate
2000-11-10	wenzelm	2000-11-10	improved cong_definition theorems; overloaded standard operations;	file \| diff \| annotate
2000-11-04	wenzelm	2000-11-04	tuned;	file \| diff \| annotate
2000-11-03	wenzelm	2000-11-03	tuned;	file \| diff \| annotate
2000-10-25	wenzelm	2000-10-25	tuned names;	file \| diff \| annotate
2000-10-23	wenzelm	2000-10-23	tuned;	file \| diff \| annotate
2000-10-22	wenzelm	2000-10-22	tuned;	file \| diff \| annotate
2000-10-22	wenzelm	2000-10-22	simplified quotients (only plain total equivs);	file \| diff \| annotate
2000-10-19	wenzelm	2000-10-19	improved typedef; tuned proofs;	file \| diff \| annotate
2000-10-18	wenzelm	2000-10-18	Quotient types;	file \| diff \| annotate

isabelle

RSS Atom