--- a/src/HOL/HOL.thy Mon Nov 05 22:49:28 2007 +0100 +++ b/src/HOL/HOL.thy Mon Nov 05 22:50:00 2007 +0100 @@ -46,6 +46,8 @@ bool :: type "fun" :: (type, type) type + itself :: (type) type + judgment Trueprop :: "bool => prop" ("(_)" 5)