src/HOL/Fun.thy
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code`
Mon, 23 Jun 2008 23:45:39 +0200 wenzelm Logic.all/mk_equals/mk_implies;
Fri, 13 Jun 2008 15:22:07 +0200 nipkow hide -> hide (open)
Thu, 12 Jun 2008 14:10:41 +0200 nipkow Hid swap
Tue, 10 Jun 2008 19:15:18 +0200 wenzelm tuned proofs -- case_tac *is* available here;
Tue, 10 Jun 2008 15:30:56 +0200 haftmann removed some dubious code lemmas
Wed, 09 Apr 2008 08:10:11 +0200 haftmann removed syntax from monad combinators; renamed mbind to scomp
Thu, 20 Mar 2008 12:04:53 +0100 haftmann added forward composition
Wed, 19 Mar 2008 22:50:42 +0100 wenzelm more antiquotations;
Tue, 26 Feb 2008 20:38:12 +0100 haftmann moved some set lemmas to Set.thy
Thu, 21 Feb 2008 17:33:58 +0100 nipkow moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
Thu, 10 Jan 2008 19:10:08 +0100 berghofe Added test data generator for function type (from Pure/codegen.ML).
Wed, 15 Aug 2007 12:52:56 +0200 paulson ATP blacklisting is now in theory data, attribute noatp
Sat, 28 Jul 2007 20:40:19 +0200 wenzelm simproc_setup fun_upd2;
Fri, 20 Jul 2007 14:27:56 +0200 haftmann simplified HOL bootstrap
Wed, 11 Jul 2007 11:02:07 +0200 berghofe Added ML bindings for sup_fun_eq and sup_bool_eq.
Wed, 09 May 2007 07:53:06 +0200 haftmann moved recfun_codegen.ML to Code_Generator.thy
Sun, 06 May 2007 21:50:17 +0200 haftmann changed code generator invocation syntax
Fri, 20 Apr 2007 11:21:42 +0200 haftmann Isar definitions are now added explicitly to code theorem table
Wed, 04 Apr 2007 00:10:59 +0200 wenzelm ML antiquotes;
Fri, 16 Mar 2007 21:32:09 +0100 haftmann moved lattice instance here
Wed, 27 Dec 2006 19:09:55 +0100 haftmann explizit serialization for Haskell id
Mon, 18 Dec 2006 08:21:26 +0100 haftmann infix syntax for generated code for composition
Mon, 27 Nov 2006 13:42:39 +0100 haftmann moved order arities for fun and bool to Fun/Orderings
Mon, 13 Nov 2006 15:43:04 +0100 haftmann dropped Typedef dependency
Tue, 07 Nov 2006 11:47:57 +0100 wenzelm renamed 'const_syntax' to 'notation';
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:32 +0200 wenzelm replaced syntax/translations by abbreviation;
Sat, 08 Apr 2006 22:51:06 +0200 wenzelm refined 'abbreviation';
Thu, 23 Mar 2006 20:03:53 +0100 nipkow Converted translations to abbbreviations.
Fri, 11 Nov 2005 00:09:37 +0100 huffman add header
Fri, 21 Oct 2005 18:14:34 +0200 wenzelm Goal.prove;
Mon, 17 Oct 2005 23:10:15 +0200 wenzelm Simplifier.inherit_context instead of Simplifier.inherit_bounds;
Thu, 22 Sep 2005 23:56:15 +0200 nipkow renamed rules to iprover
Tue, 16 Aug 2005 15:36:28 +0200 paulson classical rules must have names for ATP integration
Mon, 01 Aug 2005 19:20:26 +0200 wenzelm simprocs: Simplifier.inherit_bounds;
Thu, 07 Jul 2005 12:39:17 +0200 nipkow linear arithmetic now takes "&" in assumptions apart.
Sun, 10 Apr 2005 17:19:03 +0200 nipkow _(_|_) is now override_on
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Wed, 09 Feb 2005 18:32:28 +0100 paulson new foldSet proofs
Fri, 14 Jan 2005 12:00:27 +0100 nipkow made diff_less a simp rule
Sun, 21 Nov 2004 15:44:20 +0100 nipkow added lemmas
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, 04 Aug 2004 19:11:02 +0200 nipkow added some inj_on thms
Wed, 14 Apr 2004 14:13:05 +0200 kleing use more symbols in HTML output
Mon, 14 Apr 2003 18:52:13 +0200 nipkow Added thms
Thu, 10 Oct 2002 14:21:20 +0200 berghofe - Added range_ex1_eq
Thu, 26 Sep 2002 10:51:29 +0200 paulson Converted Fun to Isar style.
Tue, 11 Dec 2001 13:43:00 +0100 wenzelm oops;
Mon, 10 Dec 2001 20:59:43 +0100 wenzelm bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
Sat, 01 Dec 2001 18:52:32 +0100 wenzelm renamed class "term" to "type" (actually "HOL.type");
Wed, 21 Nov 2001 00:33:40 +0100 wenzelm got rid of theory Inverse_Image;
Fri, 09 Nov 2001 00:09:47 +0100 wenzelm eliminated old "symbols" syntax, use "xsymbols" instead;
Thu, 27 Sep 2001 22:28:16 +0200 wenzelm eliminated theories "equalities" and "mono" (made part of "Typedef",
Wed, 25 Jul 2001 13:13:01 +0200 paulson partial restructuring to reduce dependence on Axiom of Choice
Wed, 14 Feb 2001 20:45:35 +0100 oheimb removed whitespace
Mon, 08 Jan 2001 12:27:36 +0100 nipkow Removed Applyall
Thu, 12 Oct 2000 18:38:23 +0200 nipkow *** empty log message ***
less more (0) -60 tip