isabelle: src/HOL/Main.thy@e1f3714bc508

     1 header {* Main HOL *}

     3 theory Main

     4 imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix Coinduction Cardinal_Arithmetic_FP

     5 begin

     7 text {*

     8   Classical Higher-order Logic -- only ``Main'', excluding real and

     9   complex numbers etc.

    10 *}

    12 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}

    14 no_notation

    15   bot ("\<bottom>") and

    16   top ("\<top>") and

    17   inf (infixl "\<sqinter>" 70) and

    18   sup (infixl "\<squnion>" 65) and

    19   Inf ("\<Sqinter>_" [900] 900) and

    20   Sup ("\<Squnion>_" [900] 900)

    22 no_syntax (xsymbols)

    23   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)

    24   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)

    25   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)

    26   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)

    28 end

author	blanchet
	Mon Jan 20 18:24:55 2014 +0100 (2014-01-20)
changeset 55054	e1f3714bc508
parent 55018	2a526bd279ed
child 55056	b5c94200d081
permissions	-rw-r--r--