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