src/HOL/Nitpick.thy
changeset 44016 51184010c609
parent 44013 5cfc1c36ae97
child 44278 1220ecb81e8f
     1.1 --- a/src/HOL/Nitpick.thy	Tue Aug 02 12:17:48 2011 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Tue Aug 02 12:27:24 2011 +0200
     1.3 @@ -226,7 +226,14 @@
     1.4  use "Tools/Nitpick/nitpick_tests.ML"
     1.5  use "Tools/Nitpick/nitrox.ML"
     1.6  
     1.7 -setup {* Nitpick_Isar.setup *}
     1.8 +setup {*
     1.9 +  Nitpick_Isar.setup #>
    1.10 +  Nitpick_HOL.register_ersatz_global
    1.11 +    [(@{const_name card}, @{const_name card'}),
    1.12 +     (@{const_name setsum}, @{const_name setsum'}),
    1.13 +     (@{const_name fold_graph}, @{const_name fold_graph'}),
    1.14 +     (@{const_name wf}, @{const_name wf'})]
    1.15 +*}
    1.16  
    1.17  hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
    1.18      FunBox PairBox Word prod refl' wf' card' setsum'