src/HOL/Nitpick_Examples/Manual_Nits.thy
changeset 38288 63425c4b5f57
parent 38284 9f98107ad8b4
child 39198 f967a16dfcdd
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Aug 09 12:53:16 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Aug 09 13:46:25 2010 +0200
@@ -128,7 +128,7 @@
   | my_int_postproc _ _ _ _ t = t
 *}
 
-declare {*
+declaration {*
 Nitpick_Model.register_term_postprocessor @{typ my_int} my_int_postproc
 *}
 
@@ -212,7 +212,7 @@
 "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}])
 *}