| Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
prefer more canonical names for lemmas on min/max
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 19:28:51 +0100 |
hoelzl |
support of_rat with 0 or 1 on order relations
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Mon, 16 Sep 2013 15:30:20 +0200 |
kuncar |
use lifting_forget for deregistering numeric types as a quotient type
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 17:45:22 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 15:59:22 +0200 |
kuncar |
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
|
file |
diff |
annotate
|
| Sat, 25 May 2013 17:13:34 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 13 May 2013 13:59:04 +0200 |
kuncar |
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
|
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 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
|