src/HOL/subset.thy
Wed, 25 Jul 2001 17:58:26 +0200 paulson Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
Wed, 07 Feb 2001 20:57:03 +0100 wenzelm tuned;
Mon, 23 Oct 2000 11:15:52 +0200 wenzelm isatool unsymbolize;
Mon, 23 Oct 2000 11:14:43 +0200 wenzelm added type_definitionI;
Fri, 20 Oct 2000 19:46:53 +0200 wenzelm tuned;
Thu, 19 Oct 2000 21:22:05 +0200 wenzelm added theory for HOL type definitions;
Thu, 07 Sep 2000 20:52:02 +0200 wenzelm added linorder_cases;
Tue, 05 Oct 1999 15:29:46 +0200 berghofe Added attribute rulify_prems (useful for modifying premises of introduction
Mon, 04 Oct 1999 21:46:49 +0200 wenzelm Tools/typedef_package.ML;
Fri, 13 Nov 1998 13:27:03 +0100 paulson no longer loads Fun so that the Fun proofs can use equalities.thy
Mon, 05 Feb 1996 21:27:16 +0100 clasohm expanded tabs; renamed subtype to typedef;
Fri, 03 Mar 1995 12:02:25 +0100 clasohm new version of HOL with curried function application
less more (0) tip