equal
deleted
inserted
replaced
1 header {* Main HOL *} |
1 header {* Main HOL *} |
2 |
2 |
3 theory Main |
3 theory Main |
4 imports Plain Predicate_Compile Nitpick |
4 imports Predicate_Compile Nitpick Extraction |
5 begin |
5 begin |
6 |
6 |
7 text {* |
7 text {* |
8 Classical Higher-order Logic -- only ``Main'', excluding real and |
8 Classical Higher-order Logic -- only ``Main'', excluding real and |
9 complex numbers etc. |
9 complex numbers etc. |
10 *} |
10 *} |
11 |
11 |
12 text {* See further \cite{Nipkow-et-al:2002:tutorial} *} |
12 text {* See further \cite{Nipkow-et-al:2002:tutorial} *} |
13 |
13 |
|
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) |
|
21 |
|
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) |
|
27 |
14 end |
28 end |