isabelle: File revisions

src/ZF/equalities.thy

2010-03-13	wenzelm	2010-03-13	removed old CVS Ids; tuned headers;	file \| diff \| annotate
2007-10-07	wenzelm	2007-10-07	modernized specifications; removed legacy ML bindings;	file \| diff \| annotate
2005-06-17	haftmann	2005-06-17	migrated theory headers to new format	file \| diff \| annotate
2004-06-08	paulson	2004-06-08	Groups, Rings and supporting lemmas	file \| diff \| annotate
2003-08-28	skalberg	2003-08-28	Extended the notion of letter and digit, such that now one may use greek, gothic, euler, or calligraphic letters as normal letters.	file \| diff \| annotate
2003-07-10	paulson	2003-07-10	Changed many Intersection rules from i:I to I~=0 to avoid introducing a new variable	file \| diff \| annotate
2003-06-30	paulson	2003-06-30	Removal of UNITY/UNITYMisc, moving its theorems elsewhere. Conversion of UNITY/State to Isar format.;	file \| diff \| annotate
2003-06-27	paulson	2003-06-27	Conversion of theory UNITY to Isar script	file \| diff \| annotate
2003-06-27	paulson	2003-06-27	Conversion of AllocBase to new-style	file \| diff \| annotate
2003-06-24	paulson	2003-06-24	Converting ZF/UNITY to Isar	file \| diff \| annotate
2003-05-27	paulson	2003-05-27	updating ZF-UNITY with Sidi's new material	file \| diff \| annotate
2003-04-23	paulson	2003-04-23	Got rid of the [iff], which was effectively inserting converseD	file \| diff \| annotate
2002-10-01	paulson	2002-10-01	Numerous cosmetic changes, prompted by the new simplifier	file \| diff \| annotate
2002-09-30	berghofe	2002-09-30	Adapted to new simplifier.	file \| diff \| annotate
2002-08-28	paulson	2002-08-28	various new lemmas for Constructible	file \| diff \| annotate
2002-07-14	paulson	2002-07-14	Removal of mono.thy	file \| diff \| annotate
2002-07-14	paulson	2002-07-14	improved presentation markup	file \| diff \| annotate
2002-06-29	paulson	2002-06-29	conversion of many files to Isar format	file \| diff \| annotate
2002-06-26	paulson	2002-06-26	new theorems	file \| diff \| annotate
2002-06-05	paulson	2002-06-05	Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.	file \| diff \| annotate
2002-05-24	paulson	2002-05-24	new quantifier lemmas	file \| diff \| annotate
2002-05-22	paulson	2002-05-22	more tidying	file \| diff \| annotate
2002-05-22	paulson	2002-05-22	tidying up	file \| diff \| annotate
2002-05-21	paulson	2002-05-21	conversion of OrdQuant.ML to Isar	file \| diff \| annotate
2002-05-21	paulson	2002-05-21	converted domrange to Isar and merged with equalities	file \| diff \| annotate
2002-05-20	paulson	2002-05-20	conversion of equalities and WF to Isar	file \| diff \| annotate
1997-01-03	paulson	1997-01-03	Implicit simpsets and clasets for FOL and ZF	file \| diff \| annotate
1994-08-15	lcp	1994-08-15	ZF/equalities/Sigma_cons: new ZF/equalities/cons_eq: new ZF/equalities.thy: added final newline	file \| diff \| annotate
1993-11-16	clasohm	1993-11-16	made pseudo theories for all ML files; documented dependencies between all thy and ML files	file \| diff \| annotate

isabelle

RSS Atom