src/HOL/RealDef.thy
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Thu, 10 May 2012 09:10:43 +0200 huffman convert real number theory to use lifting/transfer
Mon, 07 May 2012 15:04:17 +0200 huffman tuned ordering of lemmas
Wed, 18 Apr 2012 14:29:20 +0200 hoelzl add lemmas to remove real conversions when compared to power of numerals
Wed, 18 Apr 2012 14:29:20 +0200 hoelzl add simp rules to rewrite comparisons of 1 and real
Mon, 16 Apr 2012 11:24:57 +0200 huffman tuned some proofs;
Thu, 12 Apr 2012 07:33:14 +0200 huffman remove outdated comment
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;
Thu, 29 Dec 2011 10:47:55 +0100 haftmann attribute code_abbrev superseedes code_unfold_post
Wed, 14 Dec 2011 10:18:28 +0100 blanchet fixed Nitpick definition of "<" on "real"s
Mon, 12 Dec 2011 13:45:54 +0100 bulwahn hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
Wed, 19 Oct 2011 09:11:14 +0200 bulwahn removing old code generator setup for real numbers; tuned
Thu, 22 Sep 2011 14:12:16 -0700 huffman discontinued legacy theorem names from RealDef.thy
Wed, 07 Sep 2011 09:45:39 -0700 huffman remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
Tue, 06 Sep 2011 19:03:41 -0700 huffman avoid using legacy theorem names
Sat, 20 Aug 2011 15:19:35 -0700 huffman replace lemma realpow_two_diff with new lemma square_diff_square_factored
Sat, 20 Aug 2011 15:54:26 -0700 huffman remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
Sat, 20 Aug 2011 13:07:00 -0700 huffman move lemma add_eq_0_iff to Groups.thy
Sat, 20 Aug 2011 12:51:15 -0700 huffman remove redundant lemma realpow_two_disj, use square_eq_iff or power2_eq_iff instead
Sat, 20 Aug 2011 10:08:47 -0700 huffman rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
Sat, 20 Aug 2011 07:09:44 -0700 huffman remove some over-specific rules from the simpset
Thu, 18 Aug 2011 13:55:26 +0200 haftmann observe distinction between sets and predicates more properly
Mon, 18 Jul 2011 10:34:21 +0200 bulwahn adding narrowing instances for real and rational
Sat, 09 Jul 2011 19:28:33 +0200 bulwahn adding code equations to execute floor and ceiling on rational and real numbers
Sat, 09 Jul 2011 13:41:58 +0200 bulwahn adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
Fri, 08 Apr 2011 16:31:14 +0200 bulwahn rational and real instances for new compilation scheme for exhaustive quickcheck
Fri, 25 Mar 2011 15:22:09 +0100 noschinl Change coercion for RealDef to use function application (not composition)
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn moving exhaustive_generators.ML to Quickcheck directory
Mon, 21 Feb 2011 10:44:19 +0100 blanchet renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
Fri, 14 Jan 2011 15:44:47 +0100 wenzelm eliminated global prems;
Fri, 17 Dec 2010 12:14:18 +0100 bulwahn adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
Mon, 06 Dec 2010 19:54:48 +0100 hoelzl move coercions to appropriate places
Mon, 06 Dec 2010 19:18:02 +0100 nipkow moved coercion decl. for int
Fri, 03 Dec 2010 17:59:13 +0100 wenzelm setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
Wed, 01 Dec 2010 20:59:29 +0100 nipkow moved activation of coercion inference into RealDef and declared function real a coercion.
Tue, 30 Nov 2010 18:40:23 +0100 haftmann merged
Mon, 29 Nov 2010 22:41:17 +0100 haftmann replaced slightly odd locale congruent2 by plain definition
Mon, 29 Nov 2010 22:32:06 +0100 haftmann replaced slightly odd locale congruent by plain definition
Mon, 29 Nov 2010 13:44:54 +0100 haftmann equivI has replaced equiv.intro
Tue, 30 Nov 2010 08:35:04 -0800 huffman use new 'file' antiquotation for reference to Dedekind_Real.thy
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations
Mon, 09 Aug 2010 12:53:16 +0200 blanchet replace "setup" with "declaration"
Fri, 06 Aug 2010 17:23:11 +0200 blanchet adapt occurrences of renamed Nitpick functions
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Mon, 12 Jul 2010 08:58:13 +0200 haftmann dropped superfluous [code del]s
Fri, 09 Jul 2010 08:11:10 +0200 haftmann nicer xsymbol syntax for fcomp and scomp
Fri, 11 Jun 2010 17:05:11 +0200 blanchet adjust Nitpick's handling of "<" on "rat"s and "reals"
Mon, 17 May 2010 18:59:59 -0700 huffman declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
Sat, 15 May 2010 07:48:24 -0700 huffman add real_le_linear to list of legacy theorem names
Tue, 11 May 2010 18:06:58 -0700 huffman no more RealPow.thy (remaining lemmas moved to RealDef.thy)
Mon, 10 May 2010 14:53:33 -0700 huffman add real_mult_commute to legacy theorem names
Mon, 10 May 2010 12:12:58 -0700 huffman new construction of real numbers using Cauchy sequences
Sun, 09 May 2010 14:21:44 -0700 huffman remove a couple of redundant lemmas; simplify some proofs
Tue, 27 Apr 2010 09:49:36 +0200 haftmann tuned class linordered_field_inverse_zero
Mon, 26 Apr 2010 15:37:50 +0200 haftmann use new classes (linordered_)field_inverse_zero
Mon, 26 Apr 2010 11:34:17 +0200 haftmann class division_ring_inverse_zero
Sun, 07 Mar 2010 09:21:16 -0800 huffman add simp rules about Ints, Nats
Tue, 23 Feb 2010 10:37:25 -0800 huffman moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
less more (0) -60 tip