# 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 \ 'a \ bool) \ bot \ Q (Eps Q)" +lemma "(Q\'a \ bool) \ bot \ (Q\'a \ bool) (Eps Q)" nitpick [expect = none] sorry -lemma "(Q \ nat \ bool) \ top \ Q (Eps Q)" +lemma "(Q\nat \ bool) \ bot \ (Q\nat \ bool) (Eps Q)" nitpick [expect = none] sorry @@ -833,7 +833,7 @@ nitpick [expect = genuine] oops -lemma "(Q \ nat \ bool) (The Q)" +lemma "(Q\nat \ bool) (The Q)" nitpick [expect = genuine] oops @@ -841,7 +841,7 @@ nitpick [expect = genuine] oops -lemma "\ (Q \ nat \ bool) (The Q)" +lemma "\ (Q\nat \ bool) (The Q)" nitpick [expect = genuine] oops @@ -861,11 +861,11 @@ nitpick [expect = genuine] oops -lemma "Q = {x\'a} \ (The Q) \ (Q\'a set)" +lemma "Q = (\x\'a. x = a) \ (Q\'a \ bool) (The Q)" nitpick [expect = none] sorry -lemma "Q = {x\nat} \ (The Q) \ (Q\nat set)" +lemma "Q = (\x\nat. x = a) \ (Q\nat \ bool) (The Q)" nitpick [expect = none] sorry