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]]