src/HOL/HOL.thy
changeset 62521 6383440f41a8
parent 62390 842917225d56
child 62522 d32c23d29968
     1.1 --- a/src/HOL/HOL.thy	Sat Mar 05 19:14:04 2016 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sat Mar 05 19:58:56 2016 +0100
     1.3 @@ -155,7 +155,7 @@
     1.4    Ex  (binder "EX " 10) and
     1.5    Ex1  (binder "EX! " 10)
     1.6  
     1.7 -notation (HOL)
     1.8 +notation (input)
     1.9    All  (binder "! " 10) and
    1.10    Ex  (binder "? " 10) and
    1.11    Ex1  (binder "?! " 10)