| 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 08:31:31 +0100 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 15:27:10 +0100 |
haftmann |
reform of predicate compiler / quickcheck theories:
|
file |
diff |
annotate
|
| Fri, 23 Nov 2012 18:28:00 +0100 |
hoelzl |
add quotient_of_div
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Mon, 21 May 2012 16:37:28 +0200 |
kuncar |
use quot_del instead of ML code in Rat.thy
|
file |
diff |
annotate
|
| Thu, 10 May 2012 21:02:36 +0200 |
huffman |
simplify instance proofs for rat
|
file |
diff |
annotate
|
| Thu, 10 May 2012 21:18:41 +0200 |
huffman |
convert Rat.thy to use lift_definition/transfer
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Fri, 02 Mar 2012 09:35:35 +0100 |
bulwahn |
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
|
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, 30 Nov 2011 16:27:10 +0100 |
wenzelm |
prefer typedef without extra definition and alternative name;
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 15:38:50 +0100 |
bulwahn |
improved generators for rational numbers to generate negative numbers;
|
file |
diff |
annotate
|
| Sun, 13 Nov 2011 20:28:22 +0100 |
blanchet |
remove unsound line in Nitpick's "rat" setup
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 09:11:14 +0200 |
bulwahn |
removing old code generator setup for rational numbers; tuned
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
adding code equations for partial_term_of for rational numbers
|
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, 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, 17 Dec 2010 12:14:18 +0100 |
bulwahn |
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
|
file |
diff |
annotate
|
| Tue, 30 Nov 2010 15:58:09 +0100 |
haftmann |
adapted proofs to slightly changed definitions of congruent(2)
|
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
|
| Fri, 01 Oct 2010 16:05:25 +0200 |
haftmann |
constant `contents` renamed to `the_elem`
|
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
|