src/HOL/Main.thy
changeset 60758 d8d85a8172b5
parent 60036 218fcc645d22
child 61955 e96292f32c3c
equal deleted inserted replaced
60757:c09598a97436 60758:d8d85a8172b5
     1 section {* Main HOL *}
     1 section \<open>Main HOL\<close>
     2 
     2 
     3 theory Main
     3 theory Main
     4 imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint Filter
     4 imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint Filter
     5 begin
     5 begin
     6 
     6 
     7 text {*
     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 *}
    10 \<close>
    11 
    11 
    12 text {* See further @{cite "Nipkow-et-al:2002:tutorial"} *}
    12 text \<open>See further @{cite "Nipkow-et-al:2002:tutorial"}\<close>
    13 
    13 
    14 no_notation
    14 no_notation
    15   bot ("\<bottom>") and
    15   bot ("\<bottom>") and
    16   top ("\<top>") and
    16   top ("\<top>") and
    17   inf (infixl "\<sqinter>" 70) and
    17   inf (infixl "\<sqinter>" 70) and