wenzelm@12024: header {* Main HOL *} wenzelm@12024: nipkow@15131: theory Main blanchet@55056: imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix Coinduction BNF_Cardinal_Arithmetic nipkow@15131: begin wenzelm@9650: wenzelm@29304: text {* wenzelm@29304: Classical Higher-order Logic -- only ``Main'', excluding real and wenzelm@29304: complex numbers etc. wenzelm@29304: *} wenzelm@29304: haftmann@27367: text {* See further \cite{Nipkow-et-al:2002:tutorial} *} haftmann@25964: haftmann@51112: no_notation haftmann@51112: bot ("\") and haftmann@51112: top ("\") and haftmann@51112: inf (infixl "\" 70) and haftmann@51112: sup (infixl "\" 65) and haftmann@51112: Inf ("\_" [900] 900) and haftmann@51112: Sup ("\_" [900] 900) haftmann@51112: haftmann@51112: no_syntax (xsymbols) haftmann@51112: "_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) haftmann@51112: "_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) haftmann@51112: "_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) haftmann@51112: "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) haftmann@51112: wenzelm@9650: end