# HG changeset patch
# User blanchet
# Date 1325611998 -3600
# Node ID 680edc1622498d549146fecc6137040f727cb390
# Parent  096697aec8a74a76cb56e7bd241e3797dcde8d98
fixed type annotations

diff -r 096697aec8a7 -r 680edc162249 src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Jan 03 18:33:18 2012 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Jan 03 18:33:18 2012 +0100
@@ -821,11 +821,11 @@
 nitpick [expect = genuine]
 oops
 
-lemma "(Q \<Colon> 'a \<Rightarrow> bool) \<noteq> bot \<Longrightarrow> Q (Eps Q)"
+lemma "(Q\<Colon>'a \<Rightarrow> bool) \<noteq> bot \<Longrightarrow> (Q\<Colon>'a \<Rightarrow> bool) (Eps Q)"
 nitpick [expect = none]
 sorry
 
-lemma "(Q \<Colon> nat \<Rightarrow> bool) \<noteq> top \<Longrightarrow> Q (Eps Q)"
+lemma "(Q\<Colon>nat \<Rightarrow> bool) \<noteq> bot \<Longrightarrow> (Q\<Colon>nat \<Rightarrow> bool) (Eps Q)"
 nitpick [expect = none]
 sorry
 
@@ -833,7 +833,7 @@
 nitpick [expect = genuine]
 oops
 
-lemma "(Q \<Colon> nat \<Rightarrow> bool) (The Q)"
+lemma "(Q\<Colon>nat \<Rightarrow> bool) (The Q)"
 nitpick [expect = genuine]
 oops
 
@@ -841,7 +841,7 @@
 nitpick [expect = genuine]
 oops
 
-lemma "\<not> (Q \<Colon> nat \<Rightarrow> bool) (The Q)"
+lemma "\<not> (Q\<Colon>nat \<Rightarrow> bool) (The Q)"
 nitpick [expect = genuine]
 oops
 
@@ -861,11 +861,11 @@
 nitpick [expect = genuine]
 oops
 
-lemma "Q = {x\<Colon>'a} \<Longrightarrow> (The Q) \<in> (Q\<Colon>'a set)"
+lemma "Q = (\<lambda>x\<Colon>'a. x = a) \<Longrightarrow> (Q\<Colon>'a \<Rightarrow> bool) (The Q)"
 nitpick [expect = none]
 sorry
 
-lemma "Q = {x\<Colon>nat} \<Longrightarrow> (The Q) \<in> (Q\<Colon>nat set)"
+lemma "Q = (\<lambda>x\<Colon>nat. x = a) \<Longrightarrow> (Q\<Colon>nat \<Rightarrow> bool) (The Q)"
 nitpick [expect = none]
 sorry