src/HOL/Quickcheck_Narrowing.thy
changeset 43314 a9090cabca14
parent 43312 7a31f9064f99
child 43315 893de45ac28d
--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 09 08:32:18 2011 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 09 08:32:19 2011 +0200
@@ -533,5 +533,6 @@
 hide_type (open) code_int narrowing_type narrowing_term cons
 hide_const (open) int_of of_int nth error toEnum map_index split_At empty
   C cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable all exists
+hide_fact empty_def
 
 end
\ No newline at end of file