changeset 67385 | deb9b0283259 |
parent 66954 | 0230af0f3c59 |
child 68980 | 5717fbc55521 |
--- a/src/HOL/Main.thy Tue Jan 09 14:07:39 2018 +0100 +++ b/src/HOL/Main.thy Tue Jan 09 15:18:41 2018 +0100 @@ -17,11 +17,6 @@ GCD begin -text \<open> - Classical Higher-order Logic -- only ``Main'', excluding real and - complex numbers etc. -\<close> - no_notation bot ("\<bottom>") and top ("\<top>") and