# HG changeset patch # User blanchet # Date 1325611998 -3600 # Node ID f1796596ef6078b355627300f5dc293acf85c818 # Parent d98eb715444dae0c3ec62ba34a7d1e153dfbf6bf tuned import diff -r d98eb715444d -r f1796596ef60 src/HOL/Nitpick_Examples/Integer_Nits.thy --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Tue Jan 03 18:33:18 2012 +0100 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Tue Jan 03 18:33:18 2012 +0100 @@ -5,10 +5,10 @@ Examples featuring Nitpick applied to natural numbers and integers. *) -header {* Examples Featuring Nitpick Applied to Natural Numbers and Integers *} +header {* Examples Featuring Nitpick Applied to Natural Numbers and Integers *} theory Integer_Nits -imports Nitpick +imports Main begin nitpick_params [verbose, card = 1\5, bits = 1,2,3,4,6,