changeset 19736 | d8d0f8f51d69 |
parent 19380 | b808efaa5828 |
child 20523 | 36a59e5d0039 |
--- a/src/HOL/ex/Higher_Order_Logic.thy Sat May 27 17:42:00 2006 +0200 +++ b/src/HOL/ex/Higher_Order_Logic.thy Sat May 27 17:42:02 2006 +0200 @@ -79,7 +79,7 @@ subsubsection {* Derived connectives *} -constdefs +definition false :: o ("\<bottom>") "\<bottom> \<equiv> \<forall>A. A" true :: o ("\<top>")