changeset 16587 | b34c8aa657a5 |
parent 16417 | 9bc16273c2d4 |
child 16633 | 208ebc9311f2 |
--- a/src/HOL/HOL.thy Tue Jun 28 15:26:45 2005 +0200 +++ b/src/HOL/HOL.thy Tue Jun 28 15:27:45 2005 +0200 @@ -33,7 +33,6 @@ Not :: "bool => bool" ("~ _" [40] 40) True :: bool False :: bool - If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) arbitrary :: 'a The :: "('a => bool) => 'a" @@ -49,6 +48,8 @@ local +consts + If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) subsubsection {* Additional concrete syntax *}