move itself into HOL types
authorkleing
Mon, 05 Nov 2007 22:50:00 +0100
changeset 25297 a5d689d04426
parent 25296 c187b7422156
child 25298 63f6d969253e
move itself into HOL types
src/HOL/HOL.thy
--- 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)