evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck.
authorbulwahn
Thu Jan 26 12:03:35 2012 +0100 (2012-01-26)
changeset 4633639fe503602fb
parent 46335 0fd9ab902b5a
child 46337 54227223a8d4
evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck.
src/HOL/Enum.thy
     1.1 --- a/src/HOL/Enum.thy	Thu Jan 26 10:59:47 2012 +0100
     1.2 +++ b/src/HOL/Enum.thy	Thu Jan 26 12:03:35 2012 +0100
     1.3 @@ -777,6 +777,7 @@
     1.4  qed
     1.5  
     1.6  code_abort enum_the
     1.7 +code_const enum_the (Eval "(fn p => raise Match)")
     1.8  
     1.9  subsection {* Further operations on finite types *}
    1.10