# HG changeset patch
# User bulwahn
# Date 1301989108 -7200
# Node ID bc1891226d00a72219827ce9affbdc9d85d0a26a
# Parent  594480d25aaa264e0650b3a148e9c044327f8a7b
removing bounded_forall code equation for characters when loading Code_Char

diff -r 594480d25aaa -r bc1891226d00 src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Tue Apr 05 09:38:23 2011 +0200
+++ b/src/HOL/Library/Code_Char.thy	Tue Apr 05 09:38:28 2011 +0200
@@ -58,4 +58,7 @@
   (Haskell "_")
   (Scala "!(_.toList)")
 
+
+declare Quickcheck_Exhaustive.char.bounded_forall_char.simps [code del]
+
 end