author | blanchet |
Mon, 20 Jan 2014 21:45:08 +0100 | |
changeset 55086 | 500ef036117b |
parent 55079 | ec08a67e993b |
child 55087 | 252c7fec4119 |
permissions | -rw-r--r-- |
12024 | 1 |
header {* Main HOL *} |
2 |
||
15131 | 3 |
theory Main |
55079 | 4 |
imports Predicate_Compile Extraction Lifting_Sum List_Prefix Coinduction Nitpick BNF_LFP BNF_GFP |
15131 | 5 |
begin |
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
6 |
|
29304 | 7 |
text {* |
8 |
Classical Higher-order Logic -- only ``Main'', excluding real and |
|
9 |
complex numbers etc. |
|
10 |
*} |
|
11 |
||
27367 | 12 |
text {* See further \cite{Nipkow-et-al:2002:tutorial} *} |
25964 | 13 |
|
55069 | 14 |
hide_const (open) |
15 |
image2 image2p vimage2p Gr Grp collect fsts snds setl setr |
|
16 |
convol pick_middlep fstOp sndOp csquare inver relImage relInvImage |
|
17 |
prefCl PrefCl Succ Shift shift proj |
|
18 |
||
51112 | 19 |
no_notation |
20 |
bot ("\<bottom>") and |
|
21 |
top ("\<top>") and |
|
22 |
inf (infixl "\<sqinter>" 70) and |
|
23 |
sup (infixl "\<squnion>" 65) and |
|
24 |
Inf ("\<Sqinter>_" [900] 900) and |
|
55057 | 25 |
Sup ("\<Squnion>_" [900] 900) and |
55065 | 26 |
ordLeq2 (infix "<=o" 50) and |
27 |
ordLeq3 (infix "\<le>o" 50) and |
|
28 |
ordLess2 (infix "<o" 50) and |
|
29 |
ordIso2 (infix "=o" 50) and |
|
55078 | 30 |
card_of ("|_|") and |
55057 | 31 |
csum (infixr "+c" 65) and |
32 |
cprod (infixr "*c" 80) and |
|
55086 | 33 |
cexp (infixr "^c" 90) and |
34 |
convol ("<_ , _>") |
|
51112 | 35 |
|
36 |
no_syntax (xsymbols) |
|
37 |
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) |
|
38 |
"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) |
|
39 |
"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) |
|
40 |
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) |
|
41 |
||
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
42 |
end |