isabelle: File revisions

src/ZF/Datatype.thy

2007-06-19	wenzelm	2007-06-19	BalancedTree;	file \| diff \| annotate
2007-04-26	wenzelm	2007-04-26	removed lagacy ML files;	file \| diff \| annotate
2005-06-17	haftmann	2005-06-17	migrated theory headers to new format	file \| diff \| annotate
2002-07-09	paulson	2002-07-09	better document preparation	file \| diff \| annotate
2001-11-14	wenzelm	2001-11-14	adapted primrec/datatype to Isar;	file \| diff \| annotate
2001-11-13	wenzelm	2001-11-13	rearranged inductive package for Isar;	file \| diff \| annotate
1999-01-07	paulson	1999-01-07	ZF: the natural numbers as a datatype	file \| diff \| annotate
1998-12-28	paulson	1998-12-28	new inductive, datatype and primrec packages, etc.	file \| diff \| annotate
1997-04-02	paulson	1997-04-02	Now a non-trivial theory so that require_thy can find it	file \| diff \| annotate
1994-12-19	lcp	1994-12-19	removed quotes around "Inductive"	file \| diff \| annotate
1994-08-25	lcp	1994-08-25	ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without the keyword "inductive" making the theory file fail ZF/Makefile: now has Inductive.thy,.ML ZF/Datatype,Finite,Zorn: depend upon Inductive ZF/intr_elim: now checks that the inductive name does not clash with existing theory names ZF/ind_section: deleted things replicated in Pure/section_utils.ML ZF/ROOT: now loads Pure/section_utils	file \| diff \| annotate
1994-08-12	lcp	1994-08-12	installation of new inductive/datatype sections	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