src/HOL/Nitpick_Examples/Special_Nits.thy
changeset 34123 8a2c5d7aff51
parent 34121 c4628a1dcf75
child 35073 cc19e2aef17e
     1.1 --- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Thu Dec 17 15:22:27 2009 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Fri Dec 18 12:00:29 2009 +0100
     1.3 @@ -135,7 +135,7 @@
     1.4  lemma "\<forall>a. g a = a
     1.5         \<Longrightarrow> \<exists>b\<^isub>1 b\<^isub>2 b\<^isub>3 b\<^isub>4 b\<^isub>5 b\<^isub>6 b\<^isub>7 b\<^isub>8 b\<^isub>9 b\<^isub>10 (b\<^isub>11\<Colon>nat).
     1.6             b\<^isub>1 < b\<^isub>11 \<and> f5 g x = f5 (\<lambda>a. if b\<^isub>1 < b\<^isub>11 then a else h b\<^isub>2) x"
     1.7 -nitpick [expect = none]
     1.8 +nitpick [expect = potential]
     1.9  nitpick [dont_specialize, expect = none]
    1.10  nitpick [dont_box, expect = none]
    1.11  nitpick [dont_box, dont_specialize, expect = none]