src/HOL/Nitpick_Examples/Core_Nits.thy
changeset 56245 84fc7dfa3cd4
parent 55893 aed17a173d16
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -292,7 +292,7 @@
     1.4  
     1.5  subsection {* Known Constants *}
     1.6  
     1.7 -lemma "x \<equiv> all \<Longrightarrow> False"
     1.8 +lemma "x \<equiv> Pure.all \<Longrightarrow> False"
     1.9  nitpick [card = 1, expect = genuine]
    1.10  nitpick [card = 1, box "('a \<Rightarrow> prop) \<Rightarrow> prop", expect = genuine]
    1.11  nitpick [card = 6, expect = genuine]
    1.12 @@ -306,15 +306,15 @@
    1.13  nitpick [expect = genuine]
    1.14  oops
    1.15  
    1.16 -lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop True"
    1.17 +lemma "Pure.all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop True"
    1.18  nitpick [expect = none]
    1.19  by auto
    1.20  
    1.21 -lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop False"
    1.22 +lemma "Pure.all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop False"
    1.23  nitpick [expect = genuine]
    1.24  oops
    1.25  
    1.26 -lemma "I = (\<lambda>x. x) \<Longrightarrow> all P \<equiv> all (\<lambda>x. P (I x))"
    1.27 +lemma "I = (\<lambda>x. x) \<Longrightarrow> Pure.all P \<equiv> Pure.all (\<lambda>x. P (I x))"
    1.28  nitpick [expect = none]
    1.29  by auto
    1.30