src/HOL/UNITY/Extend.thy
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Tue, 13 Mar 2012 23:33:35 +0100 wenzelm tuned context specifications and proofs;
Tue, 21 Feb 2012 17:09:17 +0100 wenzelm tuned proofs;
Mon, 22 Nov 2010 10:34:33 +0100 hoelzl Replace surj by abbreviation; remove surj_on.
Wed, 12 May 2010 16:44:49 +0200 wenzelm modernized specifications;
Thu, 22 Oct 2009 09:27:48 +0200 nipkow inv_onto -> inv_into
Sun, 18 Oct 2009 12:07:56 +0200 nipkow merged
Sun, 18 Oct 2009 12:07:25 +0200 nipkow Inv -> inv_onto, inv abbr. inv_onto UNIV.
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Sun, 16 Feb 2003 12:17:40 +0100 paulson minor revisions
Sat, 08 Feb 2003 16:05:33 +0100 paulson converting HOL/UNITY to use unconditional fairness
Tue, 04 Feb 2003 18:12:40 +0100 paulson some x-symbols
Fri, 31 Jan 2003 20:12:44 +0100 paulson conversion to new-style theories and tidying
less more (0) -15 tip