# HG changeset patch
# User bulwahn
# Date 1307601138 -7200
# Node ID 7a31f9064f99c2adbc9820c05d062a26b739ea52
# Parent  1efdcb579b6cc2e2446d4b62c4f601ba57469362
adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement

diff -r 1efdcb579b6c -r 7a31f9064f99 src/HOL/Quickcheck_Narrowing.thy
--- 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"