replace "setup" with "declaration"
authorblanchet
Mon, 09 Aug 2010 12:53:16 +0200
changeset 38287 796302ca3611
parent 38286 c9c7bd836894
child 38288 63425c4b5f57
replace "setup" with "declaration"
src/HOL/Library/Multiset.thy
src/HOL/Rat.thy
src/HOL/RealDef.thy
--- a/src/HOL/Library/Multiset.thy	Mon Aug 09 12:48:40 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Aug 09 12:53:16 2010 +0200
@@ -1723,8 +1723,8 @@
   | multiset_postproc _ _ _ _ t = t
 *}
 
-setup {*
-Nitpick_Model.register_term_postprocessor_global @{typ "'a multiset"}
+declaration {*
+Nitpick_Model.register_term_postprocessor @{typ "'a multiset"}
     multiset_postproc
 *}
 
--- a/src/HOL/Rat.thy	Mon Aug 09 12:48:40 2010 +0200
+++ b/src/HOL/Rat.thy	Mon Aug 09 12:53:16 2010 +0200
@@ -1173,8 +1173,8 @@
 fun rat_of_int i = (i, 1);
 *}
 
-setup {*
-  Nitpick_HOL.register_frac_type_global @{type_name rat}
+declaration {*
+  Nitpick_HOL.register_frac_type @{type_name rat}
    [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
     (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
     (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
--- a/src/HOL/RealDef.thy	Mon Aug 09 12:48:40 2010 +0200
+++ b/src/HOL/RealDef.thy	Mon Aug 09 12:53:16 2010 +0200
@@ -1795,8 +1795,8 @@
 fun real_of_int i = (i, 1);
 *}
 
-setup {*
-  Nitpick_HOL.register_frac_type_global @{type_name real}
+declaration {*
+  Nitpick_HOL.register_frac_type @{type_name real}
    [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
     (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
     (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),