| Fri, 09 Dec 2011 14:16:42 +0100 |
kuncar |
merged
|
changeset |
files
|
| Fri, 09 Dec 2011 14:14:37 +0100 |
kuncar |
make ctxt the first parameter
|
changeset |
files
|
| Fri, 09 Dec 2011 14:12:02 +0100 |
kuncar |
context/theory parametres tuned
|
changeset |
files
|
| Fri, 09 Dec 2011 14:03:17 +0100 |
kuncar |
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
|
changeset |
files
|
| Fri, 09 Dec 2011 13:42:16 +0100 |
huffman |
add induction rule for list_all2
|
changeset |
files
|
| Fri, 09 Dec 2011 12:21:03 +0100 |
bulwahn |
deactivating quickcheck_narrowing if Efficient_Nat theory is loaded
|
changeset |
files
|
| Fri, 09 Dec 2011 12:21:01 +0100 |
bulwahn |
tuned quickcheck's response
|
changeset |
files
|
| Fri, 09 Dec 2011 11:31:13 +0100 |
noschinl |
more systematic lemma name
|
changeset |
files
|
| Thu, 08 Dec 2011 13:53:28 +0100 |
bulwahn |
adding examples for quickcheck narrowing about partial functions
|
changeset |
files
|
| Thu, 08 Dec 2011 13:53:27 +0100 |
bulwahn |
removing special code generator setup for hd and last function because this causes problems with quickcheck narrowing as the Haskell Prelude functions throw errors that cannot be caught instead of PatternFail exceptions
|
changeset |
files
|
| Thu, 08 Dec 2011 13:46:04 +0100 |
huffman |
HOLCF/ex/Letrec.thy: keep class 'domain' as default sort
|
changeset |
files
|
| Thu, 08 Dec 2011 13:25:54 +0100 |
huffman |
more error checking for fixrec
|
changeset |
files
|
| Thu, 08 Dec 2011 13:25:40 +0100 |
huffman |
reinstate old functions cfst and csnd as abbreviations
|
changeset |
files
|
| Thu, 08 Dec 2011 09:10:54 +0100 |
nipkow |
merged
|
changeset |
files
|
| Thu, 08 Dec 2011 09:10:44 +0100 |
nipkow |
tuned
|
changeset |
files
|