src/HOL/Library/Float.thy
Mon, 16 Dec 2013 17:08:22 +0100 immler monotonicity of rounding and truncating float
Mon, 16 Dec 2013 17:08:22 +0100 immler Float: prevent unnecessary large numbers when adding 0
Mon, 16 Dec 2013 17:08:22 +0100 immler additional definitions and lemmas for Float
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Tue, 03 Sep 2013 22:04:23 +0200 wenzelm tuned proofs -- less guessing;
Tue, 27 Aug 2013 14:37:56 +0200 hoelzl renamed typeclass dense_linorder to unbounded_dense_linorder
Tue, 26 Mar 2013 20:02:02 +0100 wenzelm tuned imports;
Fri, 08 Mar 2013 13:21:06 +0100 kuncar patch Isabelle ditribution to conform to changes regarding the parametricity
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;
less more (0) -50 -30 tip