isabelle: File revisions

src/HOL/Induct/Com.thy

2015-10-13	haftmann	2015-10-13	prod_case as canonical name for product type eliminator	file \| diff \| annotate
2015-06-20	wenzelm	2015-06-20	isabelle update_cartouches;	file \| diff \| annotate
2015-03-25	wenzelm	2015-03-25	prefer local fixes;	file \| diff \| annotate
2014-11-02	wenzelm	2014-11-02	modernized header uniformly as section;	file \| diff \| annotate
2014-09-11	blanchet	2014-09-11	updated news	file \| diff \| annotate
2014-09-11	blanchet	2014-09-11	renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'	file \| diff \| annotate
2011-09-18	wenzelm	2011-09-18	tuned proofs;	file \| diff \| annotate
2011-08-12	huffman	2011-08-12	make more HOL theories work with separate set type	file \| diff \| annotate
2011-02-22	wenzelm	2011-02-22	modernized specifications;	file \| diff \| annotate
2010-05-12	wenzelm	2010-05-12	removed obsolete CVS Ids;	file \| diff \| annotate
2009-08-13	paulson	2009-08-13	Removal of redundant settings of unification trace and search bounds.	file \| diff \| annotate
2008-05-07	berghofe	2008-05-07	Adapted to encoding of sets as predicates	file \| diff \| annotate
2007-10-03	wenzelm	2007-10-03	avoid unnamed infixes;	file \| diff \| annotate
2007-08-07	wenzelm	2007-08-07	turned Unify flags into configuration options (global only);	file \| diff \| annotate
2007-07-11	berghofe	2007-07-11	Adapted to new inductive definition package.	file \| diff \| annotate
2006-05-27	wenzelm	2006-05-27	tuned;	file \| diff \| annotate
2005-11-25	wenzelm	2005-11-25	tuned induct proofs;	file \| diff \| annotate
2005-06-17	haftmann	2005-06-17	migrated theory headers to new format	file \| diff \| annotate
2004-04-07	paulson	2004-04-07	IsaMakefile	file \| diff \| annotate
2002-04-02	paulson	2002-04-02	conversion of some HOL/Induct proof scripts to Isar	file \| diff \| annotate
2001-12-01	wenzelm	2001-12-01	renamed class "term" to "type" (actually "HOL.type");	file \| diff \| annotate
2001-10-05	wenzelm	2001-10-05	sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;	file \| diff \| annotate
2001-08-06	nipkow	2001-08-06	turned translation for 1::nat into def. introduced 1' and replaced most occurrences of 1 by 1'.	file \| diff \| annotate
2001-01-02	nipkow	2001-01-02	* empty log message *	file \| diff \| annotate
1998-07-24	berghofe	1998-07-24	Adapted to new datatype package.	file \| diff \| annotate
1998-06-30	berghofe	1998-06-30	Adapted to new inductive definition package.	file \| diff \| annotate
1997-11-21	oheimb	1997-11-21	minor improvements of formulation and proofs	file \| diff \| annotate
1997-05-09	paulson	1997-05-09	Fixed precedence of semicolon	file \| diff \| annotate
1997-05-07	paulson	1997-05-07	New directory to contain examples of (co)inductive definitions	file \| diff \| annotate

isabelle

RSS Atom