adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement
--- a/src/HOL/Quickcheck_Narrowing.thy Thu Jun 09 08:32:16 2011 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Thu Jun 09 08:32:18 2011 +0200
@@ -3,7 +3,7 @@
header {* Counterexample generator preforming narrowing-based testing *}
theory Quickcheck_Narrowing
-imports Main "~~/src/HOL/Library/Code_Char"
+imports Quickcheck_Exhaustive
uses
("~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
("~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
@@ -26,6 +26,20 @@
code_reserved Haskell_Quickcheck Typerep
+code_type char
+ (Haskell_Quickcheck "Char")
+
+setup {*
+ fold String_Code.add_literal_char ["Haskell_Quickcheck"]
+ #> String_Code.add_literal_list_string "Haskell_Quickcheck"
+*}
+
+code_instance char :: equal
+ (Haskell_Quickcheck -)
+
+code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+ (Haskell_Quickcheck infix 4 "==")
+
subsubsection {* Type @{text "code_int"} for Haskell_Quickcheck's Int type *}
typedef (open) code_int = "UNIV \<Colon> int set"