src/HOL/Product_Type.thy
Mon, 15 Sep 2003 14:00:43 +0200 skalberg Fixed blunder in the setup of the classical reasoner wrt. the constant
Mon, 15 Sep 2003 12:27:13 +0200 skalberg Added the constant "curry".
Fri, 11 Jul 2003 14:12:41 +0200 oheimb added upd_fst, upd_snd, some thms
Thu, 08 Aug 2002 23:46:09 +0200 wenzelm use Tactic.prove instead of prove_goalw_cterm in internal proofs!
Tue, 06 Aug 2002 11:22:05 +0200 wenzelm sane interface for simprocs;
Sat, 01 Dec 2001 18:52:32 +0100 wenzelm renamed class "term" to "type" (actually "HOL.type");
Fri, 09 Nov 2001 00:09:47 +0100 wenzelm eliminated old "symbols" syntax, use "xsymbols" instead;
Sat, 27 Oct 2001 23:16:15 +0200 wenzelm tuned;
Fri, 19 Oct 2001 22:01:25 +0200 wenzelm got rid of ML proof scripts for Product_Type;
Wed, 17 Oct 2001 20:24:03 +0200 wenzelm proper proof of split_paired_all (presently unused);
Mon, 15 Oct 2001 20:33:42 +0200 wenzelm tuned;
Thu, 27 Sep 2001 22:22:58 +0200 wenzelm renamed "()" to Unity, made local;
Thu, 09 Aug 2001 10:17:45 +0200 oheimb added pair_imageI (also as intro rule)
Wed, 25 Jul 2001 13:13:01 +0200 paulson partial restructuring to reduce dependence on Axiom of Choice
Sun, 15 Jul 2001 14:47:28 +0200 wenzelm tuned;
Fri, 02 Feb 2001 22:18:10 +0100 wenzelm added hidden internal_split constant;
Thu, 01 Feb 2001 20:51:48 +0100 oheimb converted to Isar therory, adding attributes complete_split and split_format
Mon, 23 Oct 2000 11:14:00 +0200 wenzelm tuned deps;
Thu, 12 Oct 2000 18:44:35 +0200 nipkow *** empty log message ***
less more (0) tip