| Tue, 26 Mar 2013 12:20:56 +0100 |
hoelzl |
remove Real.thy
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:20:55 +0100 |
hoelzl |
merge RComplete into RealDef
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:20:54 +0100 |
hoelzl |
move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:20:52 +0100 |
hoelzl |
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
|
file |
diff |
annotate
|
| Fri, 08 Mar 2013 13:21:06 +0100 |
kuncar |
patch Isabelle ditribution to conform to changes regarding the parametricity
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 15:03:36 +0100 |
kuncar |
delete also predicates on relations when hiding an implementation of an abstract type
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 16:17:05 +0100 |
traytel |
Backed out changeset: 3fe7242f8346,
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 15:22:16 +0100 |
traytel |
coercions between base types can be lifted to sets
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 15:27:10 +0100 |
haftmann |
reform of predicate compiler / quickcheck theories:
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Thu, 10 May 2012 09:10:43 +0200 |
huffman |
convert real number theory to use lifting/transfer
|
file |
diff |
annotate
|
| Mon, 07 May 2012 15:04:17 +0200 |
huffman |
tuned ordering of lemmas
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 14:29:20 +0200 |
hoelzl |
add lemmas to remove real conversions when compared to power of numerals
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 14:29:20 +0200 |
hoelzl |
add simp rules to rewrite comparisons of 1 and real
|
file |
diff |
annotate
|
| Mon, 16 Apr 2012 11:24:57 +0200 |
huffman |
tuned some proofs;
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 07:33:14 +0200 |
huffman |
remove outdated comment
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| 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
|
| Mon, 29 Nov 2010 22:32:06 +0100 |
haftmann |
replaced slightly odd locale congruent by plain definition
|
file |
diff |
annotate
|
| Mon, 29 Nov 2010 13:44:54 +0100 |
haftmann |
equivI has replaced equiv.intro
|
file |
diff |
annotate
|
| Tue, 30 Nov 2010 08:35:04 -0800 |
huffman |
use new 'file' antiquotation for reference to Dedekind_Real.thy
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
| Mon, 09 Aug 2010 12:53:16 +0200 |
blanchet |
replace "setup" with "declaration"
|
file |
diff |
annotate
|
| Fri, 06 Aug 2010 17:23:11 +0200 |
blanchet |
adapt occurrences of renamed Nitpick functions
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Fri, 09 Jul 2010 08:11:10 +0200 |
haftmann |
nicer xsymbol syntax for fcomp and scomp
|
file |
diff |
annotate
|
| Fri, 11 Jun 2010 17:05:11 +0200 |
blanchet |
adjust Nitpick's handling of "<" on "rat"s and "reals"
|
file |
diff |
annotate
|
| Mon, 17 May 2010 18:59:59 -0700 |
huffman |
declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
|
file |
diff |
annotate
|
| Sat, 15 May 2010 07:48:24 -0700 |
huffman |
add real_le_linear to list of legacy theorem names
|
file |
diff |
annotate
|
| Tue, 11 May 2010 18:06:58 -0700 |
huffman |
no more RealPow.thy (remaining lemmas moved to RealDef.thy)
|
file |
diff |
annotate
|