src/HOL/Nitpick.thy
changeset 33561 ab01b72715ef
parent 33556 cba22e2999d5
child 33562 b1e2830ee31a
--- a/src/HOL/Nitpick.thy	Wed Oct 28 11:55:48 2009 +0100
+++ b/src/HOL/Nitpick.thy	Wed Oct 28 17:43:43 2009 +0100
@@ -8,7 +8,7 @@
 header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
 
 theory Nitpick
-imports Map SAT
+imports Map Quickcheck SAT
 uses ("Tools/Nitpick/kodkod.ML")
      ("Tools/Nitpick/kodkod_sat.ML")
      ("Tools/Nitpick/nitpick_util.ML")
@@ -241,6 +241,8 @@
 use "Tools/Nitpick/nitpick_tests.ML"
 use "Tools/Nitpick/minipick.ML"
 
+setup {* Nitpick_Isar.setup *}
+
 hide (open) const unknown undefined_fast_The undefined_fast_Eps bisim 
     bisim_iterator_max Tha refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
     fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac