src/HOL/Product_Type.thy
Thu, 19 Jan 2006 14:59:55 +0100 berghofe Re-inserted consts_code declaration accidentally deleted
Tue, 17 Jan 2006 16:36:57 +0100 haftmann substantial improvements in code generator
Thu, 29 Dec 2005 15:31:10 +0100 haftmann adaptions to changes in code generator
Thu, 08 Dec 2005 20:15:50 +0100 wenzelm tuned proofs;
Fri, 02 Dec 2005 16:05:12 +0100 haftmann adjusted to improved code generator interface
Thu, 01 Dec 2005 22:04:27 +0100 wenzelm simprocs: static evaluation of simpset;
Tue, 22 Nov 2005 12:59:25 +0100 haftmann added codegenerator
Fri, 28 Oct 2005 17:27:04 +0200 haftmann added extraction interface for code generator
Fri, 21 Oct 2005 18:14:34 +0200 wenzelm Goal.prove;
Mon, 17 Oct 2005 23:10:10 +0200 wenzelm change_claset/simpset;
Fri, 07 Oct 2005 22:59:19 +0200 wenzelm replaced _K by dummy abstraction;
Tue, 16 Aug 2005 18:53:11 +0200 paulson more simprules now have names
Wed, 03 Aug 2005 16:43:39 +0200 berghofe Fixed bug in code generator for let and split leading to ill-formed code.
Tue, 02 Aug 2005 19:47:12 +0200 wenzelm simprocs: Simplifier.inherit_bounds;
Tue, 12 Jul 2005 11:51:31 +0200 berghofe Auxiliary functions to be used in generated code are now defined using "attach".
Fri, 01 Jul 2005 13:54:57 +0200 berghofe Adapted to new interface of code generator.
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Tue, 31 May 2005 11:53:12 +0200 wenzelm tuned;
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Tue, 01 Feb 2005 18:01:57 +0100 paulson the new subst tactic, by Lucas Dixon
Sat, 18 Dec 2004 17:12:45 +0100 schirmer added print translation for split: split f --> %(x,y). f x y
Mon, 13 Dec 2004 15:06:59 +0100 paulson removal of NatArith.ML and Product_Type.ML
Fri, 10 Dec 2004 16:48:01 +0100 berghofe New code generator for let and split.
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Wed, 16 Jun 2004 14:56:39 +0200 paulson removal of x-symbol syntax <Sigma> for dependent products
Wed, 14 Apr 2004 14:13:05 +0200 kleing use more symbols in HTML output
Tue, 20 Jan 2004 13:56:27 +0100 schirmer Added print translation for pairs
Mon, 05 Jan 2004 00:46:06 +0100 nipkow undid split_comp_eq[simp] because it leads to nontermination together with split_def!
Fri, 26 Sep 2003 10:34:57 +0200 paulson misc tidying
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