# HG changeset patch
# User blanchet
# Date 1281354385 -7200
# Node ID 63425c4b5f5793696a7a2da08e6875f05246916a
# Parent  796302ca361176e2e5eb358fd722864c08d4c556
"declare" -> "declaration" (typo)

diff -r 796302ca3611 -r 63425c4b5f57 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- 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}])
 *}