author | blanchet |
Thu, 28 Aug 2014 00:40:37 +0200 | |
changeset 58055 | 625bdd5c70b2 |
parent 57641 | dc59f147b27d |
child 58128 | 43a1ba26a8cb |
permissions | -rw-r--r-- |
12024 | 1 |
header {* Main HOL *} |
2 |
||
15131 | 3 |
theory Main |
58055 | 4 |
imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick 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 |
|
51112 | 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 |
|
55057 | 20 |
Sup ("\<Squnion>_" [900] 900) and |
55065 | 21 |
ordLeq2 (infix "<=o" 50) and |
22 |
ordLeq3 (infix "\<le>o" 50) and |
|
23 |
ordLess2 (infix "<o" 50) and |
|
24 |
ordIso2 (infix "=o" 50) and |
|
55078 | 25 |
card_of ("|_|") and |
55057 | 26 |
csum (infixr "+c" 65) and |
27 |
cprod (infixr "*c" 80) and |
|
55086 | 28 |
cexp (infixr "^c" 90) and |
57641
dc59f147b27d
more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
wenzelm
parents:
57208
diff
changeset
|
29 |
convol ("\<langle>(_,/ _)\<rangle>") |
51112 | 30 |
|
55087
252c7fec4119
renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
blanchet
parents:
55086
diff
changeset
|
31 |
hide_const (open) |
55128 | 32 |
czero cinfinite cfinite csum cone ctwo Csum cprod cexp |
55087
252c7fec4119
renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
blanchet
parents:
55086
diff
changeset
|
33 |
image2 image2p vimage2p Gr Grp collect fsts snds setl setr |
56237 | 34 |
convol pick_middlep fstOp sndOp csquare relImage relInvImage |
55579
207538943038
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
traytel
parents:
55534
diff
changeset
|
35 |
Succ Shift shift proj |
55087
252c7fec4119
renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
blanchet
parents:
55086
diff
changeset
|
36 |
|
51112 | 37 |
no_syntax (xsymbols) |
38 |
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) |
|
39 |
"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) |
|
40 |
"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) |
|
41 |
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) |
|
42 |
||
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
43 |
end |