src/HOL/Main.thy
changeset 51112 da97167e03f7
parent 46155 f27cf421500a
child 53012 cb82606b8215
     1.1 --- a/src/HOL/Main.thy	Thu Feb 14 13:16:47 2013 +0100
     1.2 +++ b/src/HOL/Main.thy	Thu Feb 14 12:24:42 2013 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  header {* Main HOL *}
     1.5  
     1.6  theory Main
     1.7 -imports Plain Predicate_Compile Nitpick
     1.8 +imports Predicate_Compile Nitpick Extraction
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -11,4 +11,18 @@
    1.13  
    1.14  text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
    1.15  
    1.16 +no_notation
    1.17 +  bot ("\<bottom>") and
    1.18 +  top ("\<top>") and
    1.19 +  inf (infixl "\<sqinter>" 70) and
    1.20 +  sup (infixl "\<squnion>" 65) and
    1.21 +  Inf ("\<Sqinter>_" [900] 900) and
    1.22 +  Sup ("\<Squnion>_" [900] 900)
    1.23 +
    1.24 +no_syntax (xsymbols)
    1.25 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    1.26 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    1.27 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    1.28 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    1.29 +
    1.30  end