| Sat, 25 Feb 2012 09:07:39 +0100 |
bulwahn |
removing unnecessary assumptions in RealDef;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 10:47:55 +0100 |
haftmann |
attribute code_abbrev superseedes code_unfold_post
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 10:18:28 +0100 |
blanchet |
fixed Nitpick definition of "<" on "real"s
|
file |
diff |
annotate
|
| Mon, 12 Dec 2011 13:45:54 +0100 |
bulwahn |
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 09:11:14 +0200 |
bulwahn |
removing old code generator setup for real numbers; tuned
|
file |
diff |
annotate
|
| Thu, 22 Sep 2011 14:12:16 -0700 |
huffman |
discontinued legacy theorem names from RealDef.thy
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 19:03:41 -0700 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 15:19:35 -0700 |
huffman |
replace lemma realpow_two_diff with new lemma square_diff_square_factored
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 15:54:26 -0700 |
huffman |
remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 13:07:00 -0700 |
huffman |
move lemma add_eq_0_iff to Groups.thy
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 12:51:15 -0700 |
huffman |
remove redundant lemma realpow_two_disj, use square_eq_iff or power2_eq_iff instead
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 07:09:44 -0700 |
huffman |
remove some over-specific rules from the simpset
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:55:26 +0200 |
haftmann |
observe distinction between sets and predicates more properly
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
adding narrowing instances for real and rational
|
file |
diff |
annotate
|
| Sat, 09 Jul 2011 19:28:33 +0200 |
bulwahn |
adding code equations to execute floor and ceiling on rational and real numbers
|
file |
diff |
annotate
|
| Sat, 09 Jul 2011 13:41:58 +0200 |
bulwahn |
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:31:14 +0200 |
bulwahn |
rational and real instances for new compilation scheme for exhaustive quickcheck
|
file |
diff |
annotate
|
| Fri, 25 Mar 2011 15:22:09 +0100 |
noschinl |
Change coercion for RealDef to use function application (not composition)
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
moving exhaustive_generators.ML to Quickcheck directory
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 10:44:19 +0100 |
blanchet |
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 12:14:18 +0100 |
bulwahn |
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 19:54:48 +0100 |
hoelzl |
move coercions to appropriate places
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 19:18:02 +0100 |
nipkow |
moved coercion decl. for int
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 17:59:13 +0100 |
wenzelm |
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 20:59:29 +0100 |
nipkow |
moved activation of coercion inference into RealDef and declared function real a coercion.
|
file |
diff |
annotate
|
| Tue, 30 Nov 2010 18:40:23 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 29 Nov 2010 22:41:17 +0100 |
haftmann |
replaced slightly odd locale congruent2 by plain definition
|
file |
diff |
annotate
|