src/HOL/Main.thy
changeset 62921 499a63c30d55
parent 61955 e96292f32c3c
child 63331 247eac9758dd
equal deleted inserted replaced
62920:a5853334c179 62921:499a63c30d55
     6 
     6 
     7 text \<open>
     7 text \<open>
     8   Classical Higher-order Logic -- only ``Main'', excluding real and
     8   Classical Higher-order Logic -- only ``Main'', excluding real and
     9   complex numbers etc.
     9   complex numbers etc.
    10 \<close>
    10 \<close>
    11 
       
    12 text \<open>See further @{cite "Nipkow-et-al:2002:tutorial"}\<close>
       
    13 
    11 
    14 no_notation
    12 no_notation
    15   bot ("\<bottom>") and
    13   bot ("\<bottom>") and
    16   top ("\<top>") and
    14   top ("\<top>") and
    17   inf (infixl "\<sqinter>" 70) and
    15   inf (infixl "\<sqinter>" 70) and