| author | blanchet |
| Mon Jan 20 18:24:55 2014 +0100 (2014-01-20) | |
| changeset 55056 | b5c94200d081 |
| parent 55054 | e1f3714bc508 |
| child 55057 | 6b0fcbeebaba |
| permissions | -rw-r--r-- |
| wenzelm@12024 | 1 |
header {* Main HOL *}
|
| wenzelm@12024 | 2 |
|
| nipkow@15131 | 3 |
theory Main |
| blanchet@55056 | 4 |
imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix Coinduction BNF_Cardinal_Arithmetic |
| nipkow@15131 | 5 |
begin |
| wenzelm@9650 | 6 |
|
| wenzelm@29304 | 7 |
text {*
|
| wenzelm@29304 | 8 |
Classical Higher-order Logic -- only ``Main'', excluding real and |
| wenzelm@29304 | 9 |
complex numbers etc. |
| wenzelm@29304 | 10 |
*} |
| wenzelm@29304 | 11 |
|
| haftmann@27367 | 12 |
text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
|
| haftmann@25964 | 13 |
|
| haftmann@51112 | 14 |
no_notation |
| haftmann@51112 | 15 |
bot ("\<bottom>") and
|
| haftmann@51112 | 16 |
top ("\<top>") and
|
| haftmann@51112 | 17 |
inf (infixl "\<sqinter>" 70) and |
| haftmann@51112 | 18 |
sup (infixl "\<squnion>" 65) and |
| haftmann@51112 | 19 |
Inf ("\<Sqinter>_" [900] 900) and
|
| haftmann@51112 | 20 |
Sup ("\<Squnion>_" [900] 900)
|
| haftmann@51112 | 21 |
|
| haftmann@51112 | 22 |
no_syntax (xsymbols) |
| haftmann@51112 | 23 |
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
|
| haftmann@51112 | 24 |
"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
|
| haftmann@51112 | 25 |
"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
|
| haftmann@51112 | 26 |
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
|
| haftmann@51112 | 27 |
|
| wenzelm@9650 | 28 |
end |