src/HOL/Product_Type.thy
Fri, 25 Aug 2006 18:45:57 +0200 paulson explicit type variables prevent empty sorts
Mon, 14 Aug 2006 13:46:06 +0200 haftmann simplified code generator setup
Wed, 12 Jul 2006 17:00:22 +0200 haftmann adaptions in codegen
Sat, 08 Jul 2006 12:54:30 +0200 wenzelm simprocs: no theory argument -- use simpset context instead;
Tue, 16 May 2006 21:33:01 +0200 wenzelm tuned concrete syntax -- abbreviation/const_syntax;
Tue, 02 May 2006 20:42:30 +0200 wenzelm replaced syntax/translations by abbreviation;
Fri, 03 Mar 2006 19:30:20 +0100 nipkow changed and retracted change of location of code lemmas.
Sat, 25 Feb 2006 15:19:47 +0100 haftmann improved codegen bootstrap
Mon, 20 Feb 2006 11:38:06 +0100 haftmann slight code generator serialization improvements
Tue, 14 Feb 2006 17:07:48 +0100 haftmann added theory of executable rational numbers
Fri, 10 Feb 2006 09:09:07 +0100 haftmann improved code generator devarification
Tue, 07 Feb 2006 08:47:43 +0100 haftmann slight improvements in code generation
Mon, 23 Jan 2006 14:07:52 +0100 haftmann removed problematic keyword 'atom'
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
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;
less more (0) -60 tip