src/HOL/Library/Float.thy
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Wed, 10 Oct 2012 17:43:23 +0200 wenzelm eliminated some remaining uses of typedef with implicit set definition;
Wed, 16 May 2012 19:17:20 +0200 kuncar generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
Thu, 26 Apr 2012 14:42:50 +0200 hoelzl add code equation for real_of_float
Fri, 20 Apr 2012 11:14:39 +0200 hoelzl hide code generation facts in the Float theory, they are only exported for Approximation
Thu, 19 Apr 2012 22:13:46 +0200 hoelzl transfer now handles Let
Thu, 19 Apr 2012 18:24:40 +0200 kuncar rename no_code to no_abs_code - more appropriate name
Thu, 19 Apr 2012 11:55:30 +0200 hoelzl use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems
Wed, 18 Apr 2012 14:29:22 +0200 hoelzl use lifting to introduce floating point numbers
Wed, 18 Apr 2012 14:29:21 +0200 hoelzl replace the float datatype by a type with unique representation
Fri, 30 Mar 2012 17:22:17 +0200 wenzelm tuned proofs, less guesswork;
Tue, 27 Mar 2012 19:21:05 +0200 huffman remove redundant lemmas
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Sat, 25 Feb 2012 09:07:39 +0100 bulwahn removing unnecessary assumptions in RealDef;
Tue, 21 Feb 2012 16:28:18 +0100 wenzelm misc tuning;
Thu, 29 Dec 2011 10:47:55 +0100 haftmann attribute code_abbrev superseedes code_unfold_post
Tue, 06 Dec 2011 14:29:37 +0100 hoelzl tuned proofs
Mon, 14 Nov 2011 18:36:31 +0100 hoelzl cleaned up float theories; removed duplicate definitions and theorems
Tue, 06 Sep 2011 19:03:41 -0700 huffman avoid using legacy theorem names
Wed, 04 May 2011 15:37:39 +0200 wenzelm proper case_names for int_cases, int_of_nat_induct;
Wed, 12 Jan 2011 17:14:27 +0100 wenzelm eliminated global prems;
Mon, 06 Dec 2010 19:54:48 +0100 hoelzl move coercions to appropriate places
Mon, 06 Sep 2010 15:01:37 +0200 hoelzl When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
Sun, 09 May 2010 22:51:11 -0700 huffman avoid using real-specific versions of generic lemmas
Tue, 23 Feb 2010 10:37:25 -0800 huffman moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
Mon, 08 Feb 2010 14:06:41 +0100 haftmann separate library theory for type classes combining lattices with various algebraic structures
Tue, 10 Nov 2009 18:29:07 +0100 wenzelm eliminated some old uses of cumulative prems (!) in proof methods;
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Tue, 14 Jul 2009 16:27:32 +0200 haftmann prefer code_inline over code_unfold; use code_unfold_post where appropriate
Tue, 14 Jul 2009 10:54:04 +0200 haftmann code attributes use common underscore convention
Mon, 29 Jun 2009 23:29:11 +0200 hoelzl Implemented taylor series expansion for approximation
Thu, 04 Jun 2009 17:55:47 +0200 hoelzl Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
Wed, 29 Apr 2009 20:19:50 +0200 hoelzl replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
Wed, 29 Apr 2009 14:20:26 +0200 haftmann farewell to class recpower
Wed, 22 Apr 2009 19:09:21 +0200 haftmann power operation defined generic
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Sun, 01 Mar 2009 12:01:57 +0100 nipkow removed redundant lemmas
Thu, 26 Feb 2009 20:56:59 +0100 wenzelm standard headers;
Sat, 21 Feb 2009 09:58:26 +0100 nipkow removed redundant thms
Wed, 18 Feb 2009 20:53:58 -0800 huffman add header
Thu, 05 Feb 2009 11:45:15 +0100 hoelzl Added new Float theory and moved old Library/Float.thy to ComputeFloat
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps;
Tue, 09 Dec 2008 22:13:16 -0800 huffman move all neg-related lemmas to NatBin; make type of neg specific to int
Wed, 03 Dec 2008 21:50:36 -0800 huffman enable eq_bin_simps for simplifying equalities on numerals
Wed, 03 Dec 2008 21:00:39 -0800 huffman fix proofs related to simplification of inequalities on numerals
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
less more (0) tip