section ‹Main HOL› text ‹ Classical Higher-order Logic -- only ``Main'', excluding real and complex numbers etc. › theory Main imports Predicate_Compile Quickcheck_Narrowing Extraction Nunchaku BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices Binomial GCD begin no_notation bot ("⊥") and top ("⊤") and inf (infixl "⊓" 70) and sup (infixl "⊔" 65) and Inf ("⨅_" [900] 900) and Sup ("⨆_" [900] 900) and ordLeq2 (infix "<=o" 50) and ordLeq3 (infix "≤o" 50) and ordLess2 (infix "<o" 50) and ordIso2 (infix "=o" 50) and card_of ("|_|") and csum (infixr "+c" 65) and cprod (infixr "*c" 80) and cexp (infixr "^c" 90) and convol ("⟨(_,/ _)⟩") hide_const (open) czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift shift proj id_bnf hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV no_syntax "_INF1" :: "pttrns ⇒ 'b ⇒ 'b" ("(3⨅_./ _)" [0, 10] 10) "_INF" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b" ("(3⨅_∈_./ _)" [0, 0, 10] 10) "_SUP1" :: "pttrns ⇒ 'b ⇒ 'b" ("(3⨆_./ _)" [0, 10] 10) "_SUP" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b" ("(3⨆_∈_./ _)" [0, 0, 10] 10) end