summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Efficient_Nat.thy

changeset 48568 | 084cd758a8ab |

parent 48431 | 6efff142bb54 |

child 50023 | 28f3263d4d1b |

1.1 --- a/src/HOL/Library/Efficient_Nat.thy Fri Jul 27 21:57:56 2012 +0200 1.2 +++ b/src/HOL/Library/Efficient_Nat.thy Fri Jul 27 22:26:38 2012 +0200 1.3 @@ -281,9 +281,10 @@ 1.4 (SML "HOLogic.mk'_number/ HOLogic.natT") 1.5 1.6 text {* 1.7 - FIXME -- Evaluation with @{text "Quickcheck_Narrowing"} does not work, as 1.8 - @{text "code_module"} is very aggressive leading to bad Haskell code. 1.9 - Therefore, we simply deactivate the narrowing-based quickcheck from here on. 1.10 + Evaluation with @{text "Quickcheck_Narrowing"} does not work yet, 1.11 + since a couple of questions how to perform evaluations in Haskell are not that 1.12 + clear yet. Therefore, we simply deactivate the narrowing-based quickcheck 1.13 + from here on. 1.14 *} 1.15 1.16 declare [[quickcheck_narrowing_active = false]]