src/HOL/RealDef.thy
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
Mon, 08 Feb 2010 17:12:38 +0100 haftmann renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
Mon, 08 Feb 2010 14:06:41 +0100 haftmann separate library theory for type classes combining lattices with various algebraic structures
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Fri, 13 Nov 2009 14:14:04 +0100 nipkow renamed lemmas "anti_sym" -> "antisym"
Mon, 26 Oct 2009 20:02:37 +0100 wenzelm tuned white space;
Fri, 23 Oct 2009 18:59:24 +0200 blanchet continuation of Nitpick's integration into Isabelle;
Wed, 23 Sep 2009 14:00:12 +0200 haftmann Code_Eval(uation)
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
Tue, 07 Jul 2009 17:39:51 +0200 nipkow renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
Wed, 17 Jun 2009 16:56:15 -0700 huffman merged
Wed, 17 Jun 2009 16:55:01 -0700 huffman new GCD library, courtesy of Jeremy Avigad
Tue, 16 Jun 2009 16:26:40 +0200 haftmann denominator should not be zero
Mon, 15 Jun 2009 16:13:03 +0200 haftmann hide constant Quickcheck.random
Tue, 19 May 2009 13:57:32 +0200 haftmann moved Code_Index, Random and Quickcheck before Main
Mon, 11 May 2009 15:18:32 +0200 haftmann tuned interface of Lin_Arith
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Mon, 02 Mar 2009 16:53:55 +0100 nipkow name changes
Tue, 24 Feb 2009 11:12:58 -0800 huffman make more proofs work whether or not One_nat_def is a simp rule
less more (0) -60 tip