src/HOL/Nitpick_Examples/Manual_Nits.thy

     HOLogic.mk_number T (snd (HOLogic.dest_number t1)
                          - snd (HOLogic.dest_number t2))
   | my_int_postproc _ _ _ _ t = t
 *}
 
-declare {*
+declaration {*
 Nitpick_Model.register_term_postprocessor @{typ my_int} my_int_postproc
 *}
 
 lemma "add x y = add x x"
 nitpick [show_datatypes]

 
 lemma iterates_def [nitpick_simp]:
 "iterates f a = LCons a (iterates f (f a))"
 sorry
 
-declare {*
+declaration {*
 Nitpick_HOL.register_codatatype @{typ "'a llist"} ""
     (map dest_Const [@{term LNil}, @{term LCons}])
 *}
 
 lemma "xs \<noteq> LCons a xs"