header {* Plain HOL *}
theory Plain
imports Datatype FunDef Extraction Metis Num
begin
text {*
Plain bootstrap of fundamental HOL tools and packages; does not
include @{text Hilbert_Choice}.
*}
no_notation
bot ("⊥") and
top ("\<top>") and
inf (infixl "\<sqinter>" 70) and
sup (infixl "\<squnion>" 65) and
Inf ("\<Sqinter>_" [900] 900) and
Sup ("\<Squnion>_" [900] 900)
no_syntax (xsymbols)
"_INF1" :: "pttrns => 'b => 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
"_INF" :: "pttrn => 'a set => 'b => 'b" ("(3\<Sqinter>_∈_./ _)" [0, 0, 10] 10)
"_SUP1" :: "pttrns => 'b => 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
"_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3\<Squnion>_∈_./ _)" [0, 0, 10] 10)
end