author  wenzelm 
Tue, 31 Mar 2015 22:31:05 +0200  
changeset 59886  e0dc738eb08c 
parent 58101  e7ebe5554281 
child 60352  d46de31a50c4 
permissions  rwrr 
30293  1 
(*<*) 
30401  2 
theory Main_Doc 
30293  3 
imports Main 
4 
begin 

5 

43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset

6 
setup {* 
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset

7 
let 
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset

8 
fun pretty_term_type_only ctxt (t, T) = 
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset

9 
(if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then () 
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset

10 
else error "term_type_only: type mismatch"; 
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset

11 
Syntax.pretty_typ ctxt T) 
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset

12 
in 
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset

13 
Thy_Output.antiquotation @{binding term_type_only} 
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset

14 
(Args.term  Args.typ_abbrev) 
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset

15 
(fn {source, context = ctxt, ...} => fn arg => 
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset

16 
Thy_Output.output ctxt 
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset

17 
(Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg])) 
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset

18 
end 
30293  19 
*} 
47189
e9a3dd1c4cf9
improved robustness with new antiquoation by Makarius
nipkow
parents:
47187
diff
changeset

20 
setup {* 
e9a3dd1c4cf9
improved robustness with new antiquoation by Makarius
nipkow
parents:
47187
diff
changeset

21 
Thy_Output.antiquotation @{binding expanded_typ} (Args.typ >> single) 
e9a3dd1c4cf9
improved robustness with new antiquoation by Makarius
nipkow
parents:
47187
diff
changeset

22 
(fn {source, context, ...} => Thy_Output.output context o 
e9a3dd1c4cf9
improved robustness with new antiquoation by Makarius
nipkow
parents:
47187
diff
changeset

23 
Thy_Output.maybe_pretty_source Syntax.pretty_typ context source) 
e9a3dd1c4cf9
improved robustness with new antiquoation by Makarius
nipkow
parents:
47187
diff
changeset

24 
*} 
30293  25 
(*>*) 
26 
text{* 

27 

28 
\begin{abstract} 

54703  29 
This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. For infix operators and their precedences see the final section. The sophisticated class structure is only hinted at. For details see @{url "http://isabelle.in.tum.de/library/HOL/"}. 
30293  30 
\end{abstract} 
31 

50581  32 
\section*{HOL} 
30293  33 

30440  34 
The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P  Q"}, @{prop "P > Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}. 
35 
\smallskip 

36 

37 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

38 
@{const HOL.undefined} & @{typeof HOL.undefined}\\ 

39 
@{const HOL.default} & @{typeof HOL.default}\\ 

40 
\end{tabular} 

41 

42 
\subsubsection*{Syntax} 

30293  43 

30440  44 
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 
45 
@{term"~(x = y)"} & @{term[source]"\<not> (x = y)"} & (\verb$~=$)\\ 

46 
@{term[source]"P \<longleftrightarrow> Q"} & @{term"P \<longleftrightarrow> Q"} \\ 

47 
@{term"If x y z"} & @{term[source]"If x y z"}\\ 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51489
diff
changeset

48 
@{term"Let e\<^sub>1 (%x. e\<^sub>2)"} & @{term[source]"Let e\<^sub>1 (\<lambda>x. e\<^sub>2)"}\\ 
30440  49 
\end{supertabular} 
50 

51 

50581  52 
\section*{Orderings} 
30440  53 

54 
A collection of classes defining basic orderings: 

55 
preorder, partial order, linear order, dense linear order and wellorder. 

56 
\smallskip 

30293  57 

30425  58 
\begin{supertabular}{@ {} l @ {~::~} l l @ {}} 
35277  59 
@{const Orderings.less_eq} & @{typeof Orderings.less_eq} & (\verb$<=$)\\ 
60 
@{const Orderings.less} & @{typeof Orderings.less}\\ 

30440  61 
@{const Orderings.Least} & @{typeof Orderings.Least}\\ 
62 
@{const Orderings.min} & @{typeof Orderings.min}\\ 

63 
@{const Orderings.max} & @{typeof Orderings.max}\\ 

64 
@{const[source] top} & @{typeof Orderings.top}\\ 

65 
@{const[source] bot} & @{typeof Orderings.bot}\\ 

66 
@{const Orderings.mono} & @{typeof Orderings.mono}\\ 

67 
@{const Orderings.strict_mono} & @{typeof Orderings.strict_mono}\\ 

30293  68 
\end{supertabular} 
69 

70 
\subsubsection*{Syntax} 

71 

30440  72 
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 
73 
@{term[source]"x \<ge> y"} & @{term"x \<ge> y"} & (\verb$>=$)\\ 

30293  74 
@{term[source]"x > y"} & @{term"x > y"}\\ 
75 
@{term"ALL x<=y. P"} & @{term[source]"\<forall>x. x \<le> y \<longrightarrow> P"}\\ 

30440  76 
@{term"EX x<=y. P"} & @{term[source]"\<exists>x. x \<le> y \<and> P"}\\ 
77 
\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\ 

30293  78 
@{term"LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\ 
79 
\end{supertabular} 

80 

30401  81 

50581  82 
\section*{Lattices} 
30401  83 

84 
Classes semilattice, lattice, distributive lattice and complete lattice (the 

85 
latter in theory @{theory Set}). 

86 

87 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

88 
@{const Lattices.inf} & @{typeof Lattices.inf}\\ 

89 
@{const Lattices.sup} & @{typeof Lattices.sup}\\ 

44969  90 
@{const Complete_Lattices.Inf} & @{term_type_only Complete_Lattices.Inf "'a set \<Rightarrow> 'a::Inf"}\\ 
91 
@{const Complete_Lattices.Sup} & @{term_type_only Complete_Lattices.Sup "'a set \<Rightarrow> 'a::Sup"}\\ 

30401  92 
\end{tabular} 
93 

94 
\subsubsection*{Syntax} 

95 

30440  96 
Available by loading theory @{text Lattice_Syntax} in directory @{text 
97 
Library}. 

30401  98 

99 
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

100 
@{text[source]"x \<sqsubseteq> y"} & @{term"x \<le> y"}\\ 

101 
@{text[source]"x \<sqsubset> y"} & @{term"x < y"}\\ 

102 
@{text[source]"x \<sqinter> y"} & @{term"inf x y"}\\ 

103 
@{text[source]"x \<squnion> y"} & @{term"sup x y"}\\ 

104 
@{text[source]"\<Sqinter> A"} & @{term"Sup A"}\\ 

105 
@{text[source]"\<Squnion> A"} & @{term"Inf A"}\\ 

30440  106 
@{text[source]"\<top>"} & @{term[source] top}\\ 
107 
@{text[source]"\<bottom>"} & @{term[source] bot}\\ 

30401  108 
\end{supertabular} 
109 

110 

50581  111 
\section*{Set} 
30293  112 

30425  113 
\begin{supertabular}{@ {} l @ {~::~} l l @ {}} 
30370  114 
@{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\ 
32142  115 
@{const Set.insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\ 
30293  116 
@{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\ 
38323  117 
@{const Set.member} & @{term_type_only Set.member "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\texttt{:})\\ 
32208  118 
@{const Set.union} & @{term_type_only Set.union "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Un})\\ 
119 
@{const Set.inter} & @{term_type_only Set.inter "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Int})\\ 

30293  120 
@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\ 
121 
@{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\ 

122 
@{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\ 

123 
@{const Inter} & @{term_type_only Inter "'a set set\<Rightarrow>'a set"}\\ 

124 
@{const Pow} & @{term_type_only Pow "'a set \<Rightarrow>'a set set"}\\ 

125 
@{const UNIV} & @{term_type_only UNIV "'a set"}\\ 

126 
@{const image} & @{term_type_only image "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set"}\\ 

127 
@{const Ball} & @{term_type_only Ball "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\ 

128 
@{const Bex} & @{term_type_only Bex "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\ 

129 
\end{supertabular} 

130 

131 
\subsubsection*{Syntax} 

132 

30425  133 
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 
53328  134 
@{text"{a\<^sub>1,\<dots>,a\<^sub>n}"} & @{text"insert a\<^sub>1 (\<dots> (insert a\<^sub>n {})\<dots>)"}\\ 
135 
@{term"a ~: A"} & @{term[source]"\<not>(x \<in> A)"}\\ 

30293  136 
@{term"A \<subseteq> B"} & @{term[source]"A \<le> B"}\\ 
137 
@{term"A \<subset> B"} & @{term[source]"A < B"}\\ 

138 
@{term[source]"A \<supseteq> B"} & @{term[source]"B \<le> A"}\\ 

139 
@{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\ 

30440  140 
@{term"{x. P}"} & @{term[source]"Collect (\<lambda>x. P)"}\\ 
53328  141 
@{text"{t  x\<^sub>1 \<dots> x\<^sub>n. P}"} & @{text"{v. \<exists>x\<^sub>1 \<dots> x\<^sub>n. v = t \<and> P}"}\\ 
30425  142 
@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"} & (\texttt{UN})\\ 
30370  143 
@{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\ 
30425  144 
@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"} & (\texttt{INT})\\ 
30370  145 
@{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\ 
30293  146 
@{term"ALL x:A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\ 
147 
@{term"EX x:A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\ 

148 
@{term"range f"} & @{term[source]"f ` UNIV"}\\ 

149 
\end{supertabular} 

150 

151 

50581  152 
\section*{Fun} 
30293  153 

32933  154 
\begin{supertabular}{@ {} l @ {~::~} l l @ {}} 
30293  155 
@{const "Fun.id"} & @{typeof Fun.id}\\ 
32933  156 
@{const "Fun.comp"} & @{typeof Fun.comp} & (\texttt{o})\\ 
30293  157 
@{const "Fun.inj_on"} & @{term_type_only Fun.inj_on "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>bool"}\\ 
158 
@{const "Fun.inj"} & @{typeof Fun.inj}\\ 

159 
@{const "Fun.surj"} & @{typeof Fun.surj}\\ 

160 
@{const "Fun.bij"} & @{typeof Fun.bij}\\ 

161 
@{const "Fun.bij_betw"} & @{term_type_only Fun.bij_betw "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set\<Rightarrow>bool"}\\ 

162 
@{const "Fun.fun_upd"} & @{typeof Fun.fun_upd}\\ 

163 
\end{supertabular} 

164 

165 
\subsubsection*{Syntax} 

166 

167 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

168 
@{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\ 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51489
diff
changeset

169 
@{text"f(x\<^sub>1:=y\<^sub>1,\<dots>,x\<^sub>n:=y\<^sub>n)"} & @{text"f(x\<^sub>1:=y\<^sub>1)\<dots>(x\<^sub>n:=y\<^sub>n)"}\\ 
30293  170 
\end{tabular} 
171 

172 

50581  173 
\section*{Hilbert\_Choice} 
33019  174 

175 
Hilbert's selection ($\varepsilon$) operator: @{term"SOME x. P"}. 

176 
\smallskip 

177 

178 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

33057  179 
@{const Hilbert_Choice.inv_into} & @{term_type_only Hilbert_Choice.inv_into "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"} 
33019  180 
\end{tabular} 
181 

182 
\subsubsection*{Syntax} 

183 

184 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

33057  185 
@{term inv} & @{term[source]"inv_into UNIV"} 
33019  186 
\end{tabular} 
187 

50581  188 
\section*{Fixed Points} 
30293  189 

190 
Theory: @{theory Inductive}. 

191 

192 
Least and greatest fixed points in a complete lattice @{typ 'a}: 

193 

194 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

195 
@{const Inductive.lfp} & @{typeof Inductive.lfp}\\ 

196 
@{const Inductive.gfp} & @{typeof Inductive.gfp}\\ 

197 
\end{tabular} 

198 

199 
Note that in particular sets (@{typ"'a \<Rightarrow> bool"}) are complete lattices. 

200 

50581  201 
\section*{Sum\_Type} 
30293  202 

203 
Type constructor @{text"+"}. 

204 

205 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

206 
@{const Sum_Type.Inl} & @{typeof Sum_Type.Inl}\\ 

207 
@{const Sum_Type.Inr} & @{typeof Sum_Type.Inr}\\ 

208 
@{const Sum_Type.Plus} & @{term_type_only Sum_Type.Plus "'a set\<Rightarrow>'b set\<Rightarrow>('a+'b)set"} 

209 
\end{tabular} 

210 

211 

50581  212 
\section*{Product\_Type} 
30293  213 

214 
Types @{typ unit} and @{text"\<times>"}. 

215 

216 
\begin{supertabular}{@ {} l @ {~::~} l @ {}} 

217 
@{const Product_Type.Unity} & @{typeof Product_Type.Unity}\\ 

218 
@{const Pair} & @{typeof Pair}\\ 

219 
@{const fst} & @{typeof fst}\\ 

220 
@{const snd} & @{typeof snd}\\ 

221 
@{const split} & @{typeof split}\\ 

222 
@{const curry} & @{typeof curry}\\ 

223 
@{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\<Rightarrow>('a\<Rightarrow>'b set)\<Rightarrow>('a*'b)set"}\\ 

224 
\end{supertabular} 

225 

226 
\subsubsection*{Syntax} 

227 

30440  228 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}} 
30293  229 
@{term"Pair a b"} & @{term[source]"Pair a b"}\\ 
230 
@{term"split (\<lambda>x y. t)"} & @{term[source]"split (\<lambda>x y. t)"}\\ 

30440  231 
@{term"A <*> B"} & @{text"Sigma A (\<lambda>\<^raw:\_>. B)"} & (\verb$<*>$) 
30293  232 
\end{tabular} 
233 

234 
Pairs may be nested. Nesting to the right is printed as a tuple, 

30440  235 
e.g.\ \mbox{@{term"(a,b,c)"}} is really \mbox{@{text"(a, (b, c))"}.} 
30293  236 
Pattern matching with pairs and tuples extends to all binders, 
30440  237 
e.g.\ \mbox{@{prop"ALL (x,y):A. P"},} @{term"{(x,y). P}"}, etc. 
30293  238 

239 

50581  240 
\section*{Relation} 
30293  241 

47187  242 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 
30293  243 
@{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\ 
47682  244 
@{const Relation.relcomp} & @{term_type_only Relation.relcomp "('a*'b)set\<Rightarrow>('b*'c)set\<Rightarrow>('a*'c)set"}\\ 
30293  245 
@{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\<Rightarrow>'a set\<Rightarrow>'b set"}\\ 
246 
@{const Relation.inv_image} & @{term_type_only Relation.inv_image "('a*'a)set\<Rightarrow>('b\<Rightarrow>'a)\<Rightarrow>('b*'b)set"}\\ 

247 
@{const Relation.Id_on} & @{term_type_only Relation.Id_on "'a set\<Rightarrow>('a*'a)set"}\\ 

248 
@{const Relation.Id} & @{term_type_only Relation.Id "('a*'a)set"}\\ 

249 
@{const Relation.Domain} & @{term_type_only Relation.Domain "('a*'b)set\<Rightarrow>'a set"}\\ 

250 
@{const Relation.Range} & @{term_type_only Relation.Range "('a*'b)set\<Rightarrow>'b set"}\\ 

251 
@{const Relation.Field} & @{term_type_only Relation.Field "('a*'a)set\<Rightarrow>'a set"}\\ 

252 
@{const Relation.refl_on} & @{term_type_only Relation.refl_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\ 

253 
@{const Relation.refl} & @{term_type_only Relation.refl "('a*'a)set\<Rightarrow>bool"}\\ 

254 
@{const Relation.sym} & @{term_type_only Relation.sym "('a*'a)set\<Rightarrow>bool"}\\ 

255 
@{const Relation.antisym} & @{term_type_only Relation.antisym "('a*'a)set\<Rightarrow>bool"}\\ 

256 
@{const Relation.trans} & @{term_type_only Relation.trans "('a*'a)set\<Rightarrow>bool"}\\ 

257 
@{const Relation.irrefl} & @{term_type_only Relation.irrefl "('a*'a)set\<Rightarrow>bool"}\\ 

258 
@{const Relation.total_on} & @{term_type_only Relation.total_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\ 

30440  259 
@{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\<Rightarrow>bool"}\\ 
47187  260 
\end{tabular} 
30293  261 

262 
\subsubsection*{Syntax} 

263 

30440  264 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 
265 
@{term"converse r"} & @{term[source]"converse r"} & (\verb$^1$) 

30293  266 
\end{tabular} 
47187  267 
\medskip 
268 

269 
\noindent 

47189
e9a3dd1c4cf9
improved robustness with new antiquoation by Makarius
nipkow
parents:
47187
diff
changeset

270 
Type synonym \ @{typ"'a rel"} @{text"="} @{expanded_typ "'a rel"} 
30293  271 

50581  272 
\section*{Equiv\_Relations} 
30293  273 

274 
\begin{supertabular}{@ {} l @ {~::~} l @ {}} 

275 
@{const Equiv_Relations.equiv} & @{term_type_only Equiv_Relations.equiv "'a set \<Rightarrow> ('a*'a)set\<Rightarrow>bool"}\\ 

276 
@{const Equiv_Relations.quotient} & @{term_type_only Equiv_Relations.quotient "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"}\\ 

277 
@{const Equiv_Relations.congruent} & @{term_type_only Equiv_Relations.congruent "('a*'a)set\<Rightarrow>('a\<Rightarrow>'b)\<Rightarrow>bool"}\\ 

278 
@{const Equiv_Relations.congruent2} & @{term_type_only Equiv_Relations.congruent2 "('a*'a)set\<Rightarrow>('b*'b)set\<Rightarrow>('a\<Rightarrow>'b\<Rightarrow>'c)\<Rightarrow>bool"}\\ 

279 
%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\ 

280 
\end{supertabular} 

281 

282 
\subsubsection*{Syntax} 

283 

284 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

285 
@{term"congruent r f"} & @{term[source]"congruent r f"}\\ 

286 
@{term"congruent2 r r f"} & @{term[source]"congruent2 r r f"}\\ 

287 
\end{tabular} 

288 

289 

50581  290 
\section*{Transitive\_Closure} 
30293  291 

292 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

293 
@{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ 

294 
@{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ 

295 
@{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ 

45618  296 
@{const Transitive_Closure.acyclic} & @{term_type_only Transitive_Closure.acyclic "('a*'a)set\<Rightarrow>bool"}\\ 
30988  297 
@{const compower} & @{term_type_only "op ^^ :: ('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set" "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set"}\\ 
30293  298 
\end{tabular} 
299 

300 
\subsubsection*{Syntax} 

301 

30440  302 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 
303 
@{term"rtrancl r"} & @{term[source]"rtrancl r"} & (\verb$^*$)\\ 

304 
@{term"trancl r"} & @{term[source]"trancl r"} & (\verb$^+$)\\ 

305 
@{term"reflcl r"} & @{term[source]"reflcl r"} & (\verb$^=$) 

30293  306 
\end{tabular} 
307 

308 

50581  309 
\section*{Algebra} 
30293  310 

35061  311 
Theories @{theory Groups}, @{theory Rings}, @{theory Fields} and @{theory 
30440  312 
Divides} define a large collection of classes describing common algebraic 
313 
structures from semigroups up to fields. Everything is done in terms of 

314 
overloaded operators: 

315 

316 
\begin{supertabular}{@ {} l @ {~::~} l l @ {}} 

317 
@{text "0"} & @{typeof zero}\\ 

318 
@{text "1"} & @{typeof one}\\ 

319 
@{const plus} & @{typeof plus}\\ 

320 
@{const minus} & @{typeof minus}\\ 

321 
@{const uminus} & @{typeof uminus} & (\verb$$)\\ 

322 
@{const times} & @{typeof times}\\ 

323 
@{const inverse} & @{typeof inverse}\\ 

324 
@{const divide} & @{typeof divide}\\ 

325 
@{const abs} & @{typeof abs}\\ 

326 
@{const sgn} & @{typeof sgn}\\ 

327 
@{const dvd_class.dvd} & @{typeof "dvd_class.dvd"}\\ 

328 
@{const div_class.div} & @{typeof "div_class.div"}\\ 

329 
@{const div_class.mod} & @{typeof "div_class.mod"}\\ 

330 
\end{supertabular} 

331 

332 
\subsubsection*{Syntax} 

333 

334 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

335 
@{term"abs x"} & @{term[source]"abs x"} 

336 
\end{tabular} 

30293  337 

338 

50581  339 
\section*{Nat} 
30293  340 

341 
@{datatype nat} 

342 
\bigskip 

343 

344 
\begin{tabular}{@ {} lllllll @ {}} 

345 
@{term "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"} & 

346 
@{term "op  :: nat \<Rightarrow> nat \<Rightarrow> nat"} & 

347 
@{term "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"} & 

47187  348 
@{term "op ^ :: nat \<Rightarrow> nat \<Rightarrow> nat"} & 
30293  349 
@{term "op div :: nat \<Rightarrow> nat \<Rightarrow> nat"}& 
350 
@{term "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}& 

351 
@{term "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"}\\ 

352 
@{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"} & 

353 
@{term "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"} & 

354 
@{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} & 

355 
@{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"} & 

356 
@{term "Min :: nat set \<Rightarrow> nat"} & 

357 
@{term "Max :: nat set \<Rightarrow> nat"}\\ 

358 
\end{tabular} 

359 

360 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

30988  361 
@{const Nat.of_nat} & @{typeof Nat.of_nat}\\ 
362 
@{term "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"} & 

363 
@{term_type_only "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"} 

30293  364 
\end{tabular} 
365 

50581  366 
\section*{Int} 
30293  367 

368 
Type @{typ int} 

369 
\bigskip 

370 

371 
\begin{tabular}{@ {} llllllll @ {}} 

372 
@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} & 

373 
@{term "op  :: int \<Rightarrow> int \<Rightarrow> int"} & 

374 
@{term "uminus :: int \<Rightarrow> int"} & 

375 
@{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} & 

376 
@{term "op ^ :: int \<Rightarrow> nat \<Rightarrow> int"} & 

377 
@{term "op div :: int \<Rightarrow> int \<Rightarrow> int"}& 

378 
@{term "op mod :: int \<Rightarrow> int \<Rightarrow> int"}& 

379 
@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"}\\ 

380 
@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} & 

381 
@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} & 

382 
@{term "min :: int \<Rightarrow> int \<Rightarrow> int"} & 

383 
@{term "max :: int \<Rightarrow> int \<Rightarrow> int"} & 

384 
@{term "Min :: int set \<Rightarrow> int"} & 

385 
@{term "Max :: int set \<Rightarrow> int"}\\ 

386 
@{term "abs :: int \<Rightarrow> int"} & 

387 
@{term "sgn :: int \<Rightarrow> int"}\\ 

388 
\end{tabular} 

389 

30440  390 
\begin{tabular}{@ {} l @ {~::~} l l @ {}} 
30293  391 
@{const Int.nat} & @{typeof Int.nat}\\ 
392 
@{const Int.of_int} & @{typeof Int.of_int}\\ 

30440  393 
@{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"} & (\verb$Ints$) 
30293  394 
\end{tabular} 
395 

396 
\subsubsection*{Syntax} 

397 

398 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

399 
@{term"of_nat::nat\<Rightarrow>int"} & @{term[source]"of_nat"}\\ 

400 
\end{tabular} 

401 

402 

50581  403 
\section*{Finite\_Set} 
30401  404 

405 

406 
\begin{supertabular}{@ {} l @ {~::~} l @ {}} 

407 
@{const Finite_Set.finite} & @{term_type_only Finite_Set.finite "'a set\<Rightarrow>bool"}\\ 

408 
@{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set => nat"}\\ 

409 
@{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\ 

54744
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
54703
diff
changeset

410 
@{const Groups_Big.setsum} & @{term_type_only Groups_Big.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\ 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
54703
diff
changeset

411 
@{const Groups_Big.setprod} & @{term_type_only Groups_Big.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\ 
30401  412 
\end{supertabular} 
413 

414 

415 
\subsubsection*{Syntax} 

416 

30440  417 
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 
418 
@{term"setsum (%x. x) A"} & @{term[source]"setsum (\<lambda>x. x) A"} & (\verb$SUM$)\\ 

30401  419 
@{term"setsum (%x. t) A"} & @{term[source]"setsum (\<lambda>x. t) A"}\\ 
420 
@{term[source]"\<Sum>xP. t"} & @{term"\<Sum>xP. t"}\\ 

30440  421 
\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}} & (\verb$PROD$)\\ 
30401  422 
\end{supertabular} 
423 

424 

50581  425 
\section*{Wellfounded} 
30293  426 

427 
\begin{supertabular}{@ {} l @ {~::~} l @ {}} 

428 
@{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\<Rightarrow>bool"}\\ 

429 
@{const Wellfounded.acc} & @{term_type_only Wellfounded.acc "('a*'a)set\<Rightarrow>'a set"}\\ 

430 
@{const Wellfounded.measure} & @{term_type_only Wellfounded.measure "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set"}\\ 

431 
@{const Wellfounded.lex_prod} & @{term_type_only Wellfounded.lex_prod "('a*'a)set\<Rightarrow>('b*'b)set\<Rightarrow>(('a*'b)*('a*'b))set"}\\ 

432 
@{const Wellfounded.mlex_prod} & @{term_type_only Wellfounded.mlex_prod "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set\<Rightarrow>('a*'a)set"}\\ 

433 
@{const Wellfounded.less_than} & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\ 

434 
@{const Wellfounded.pred_nat} & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\ 

435 
\end{supertabular} 

436 

437 

50581  438 
\section*{Set\_Interval} % @{theory Set_Interval} 
30321  439 

440 
\begin{supertabular}{@ {} l @ {~::~} l @ {}} 

30370  441 
@{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\ 
442 
@{const atMost} & @{term_type_only atMost "'a::ord \<Rightarrow> 'a set"}\\ 

443 
@{const greaterThan} & @{term_type_only greaterThan "'a::ord \<Rightarrow> 'a set"}\\ 

444 
@{const atLeast} & @{term_type_only atLeast "'a::ord \<Rightarrow> 'a set"}\\ 

445 
@{const greaterThanLessThan} & @{term_type_only greaterThanLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ 

446 
@{const atLeastLessThan} & @{term_type_only atLeastLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ 

447 
@{const greaterThanAtMost} & @{term_type_only greaterThanAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ 

448 
@{const atLeastAtMost} & @{term_type_only atLeastAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ 

30321  449 
\end{supertabular} 
450 

451 
\subsubsection*{Syntax} 

452 

453 
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

454 
@{term "lessThan y"} & @{term[source] "lessThan y"}\\ 

455 
@{term "atMost y"} & @{term[source] "atMost y"}\\ 

456 
@{term "greaterThan x"} & @{term[source] "greaterThan x"}\\ 

457 
@{term "atLeast x"} & @{term[source] "atLeast x"}\\ 

458 
@{term "greaterThanLessThan x y"} & @{term[source] "greaterThanLessThan x y"}\\ 

459 
@{term "atLeastLessThan x y"} & @{term[source] "atLeastLessThan x y"}\\ 

460 
@{term "greaterThanAtMost x y"} & @{term[source] "greaterThanAtMost x y"}\\ 

461 
@{term "atLeastAtMost x y"} & @{term[source] "atLeastAtMost x y"}\\ 

30370  462 
@{term[mode=xsymbols] "UN i:{..n}. A"} & @{term[source] "\<Union> i \<in> {..n}. A"}\\ 
463 
@{term[mode=xsymbols] "UN i:{..<n}. A"} & @{term[source] "\<Union> i \<in> {..<n}. A"}\\ 

464 
\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Inter>"} instead of @{text"\<Union>"}}\\ 

30321  465 
@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\ 
30370  466 
@{term "setsum (%x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\ 
30386  467 
@{term "setsum (%x. t) {..b}"} & @{term[source] "setsum (\<lambda>x. t) {..b}"}\\ 
468 
@{term "setsum (%x. t) {..<b}"} & @{term[source] "setsum (\<lambda>x. t) {..<b}"}\\ 

30372  469 
\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}}\\ 
30321  470 
\end{supertabular} 
471 

472 

50581  473 
\section*{Power} 
30293  474 

475 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

476 
@{const Power.power} & @{typeof Power.power} 

477 
\end{tabular} 

478 

479 

50581  480 
\section*{Option} 
30293  481 

482 
@{datatype option} 

483 
\bigskip 

484 

485 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

486 
@{const Option.the} & @{typeof Option.the}\\ 

55466  487 
@{const map_option} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\ 
55518
1ddb2edf5ceb
folded 'Option.set' into BNFgenerated 'set_option'
blanchet
parents:
55466
diff
changeset

488 
@{const set_option} & @{term_type_only set_option "'a option \<Rightarrow> 'a set"}\\ 
41532  489 
@{const Option.bind} & @{term_type_only Option.bind "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"} 
30293  490 
\end{tabular} 
491 

50581  492 
\section*{List} 
30293  493 

494 
@{datatype list} 

495 
\bigskip 

496 

497 
\begin{supertabular}{@ {} l @ {~::~} l @ {}} 

498 
@{const List.append} & @{typeof List.append}\\ 

499 
@{const List.butlast} & @{typeof List.butlast}\\ 

500 
@{const List.concat} & @{typeof List.concat}\\ 

501 
@{const List.distinct} & @{typeof List.distinct}\\ 

502 
@{const List.drop} & @{typeof List.drop}\\ 

503 
@{const List.dropWhile} & @{typeof List.dropWhile}\\ 

504 
@{const List.filter} & @{typeof List.filter}\\ 

47187  505 
@{const List.find} & @{typeof List.find}\\ 
46133
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
45618
diff
changeset

506 
@{const List.fold} & @{typeof List.fold}\\ 
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
45618
diff
changeset

507 
@{const List.foldr} & @{typeof List.foldr}\\ 
30293  508 
@{const List.foldl} & @{typeof List.foldl}\\ 
509 
@{const List.hd} & @{typeof List.hd}\\ 

510 
@{const List.last} & @{typeof List.last}\\ 

511 
@{const List.length} & @{typeof List.length}\\ 

512 
@{const List.lenlex} & @{term_type_only List.lenlex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ 

513 
@{const List.lex} & @{term_type_only List.lex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ 

514 
@{const List.lexn} & @{term_type_only List.lexn "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a list * 'a list)set"}\\ 

515 
@{const List.lexord} & @{term_type_only List.lexord "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ 

46488  516 
@{const List.listrel} & @{term_type_only List.listrel "('a*'b)set\<Rightarrow>('a list * 'b list)set"}\\ 
40272  517 
@{const List.listrel1} & @{term_type_only List.listrel1 "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ 
30293  518 
@{const List.lists} & @{term_type_only List.lists "'a set\<Rightarrow>'a list set"}\\ 
519 
@{const List.listset} & @{term_type_only List.listset "'a set list \<Rightarrow> 'a list set"}\\ 

58101  520 
@{const Groups_List.listsum} & @{typeof Groups_List.listsum}\\ 
30293  521 
@{const List.list_all2} & @{typeof List.list_all2}\\ 
522 
@{const List.list_update} & @{typeof List.list_update}\\ 

523 
@{const List.map} & @{typeof List.map}\\ 

524 
@{const List.measures} & @{term_type_only List.measures "('a\<Rightarrow>nat)list\<Rightarrow>('a*'a)set"}\\ 

32933  525 
@{const List.nth} & @{typeof List.nth}\\ 
30293  526 
@{const List.remdups} & @{typeof List.remdups}\\ 
527 
@{const List.removeAll} & @{typeof List.removeAll}\\ 

528 
@{const List.remove1} & @{typeof List.remove1}\\ 

529 
@{const List.replicate} & @{typeof List.replicate}\\ 

530 
@{const List.rev} & @{typeof List.rev}\\ 

531 
@{const List.rotate} & @{typeof List.rotate}\\ 

532 
@{const List.rotate1} & @{typeof List.rotate1}\\ 

533 
@{const List.set} & @{term_type_only List.set "'a list \<Rightarrow> 'a set"}\\ 

534 
@{const List.sort} & @{typeof List.sort}\\ 

535 
@{const List.sorted} & @{typeof List.sorted}\\ 

536 
@{const List.splice} & @{typeof List.splice}\\ 

537 
@{const List.sublist} & @{typeof List.sublist}\\ 

538 
@{const List.take} & @{typeof List.take}\\ 

539 
@{const List.takeWhile} & @{typeof List.takeWhile}\\ 

540 
@{const List.tl} & @{typeof List.tl}\\ 

541 
@{const List.upt} & @{typeof List.upt}\\ 

542 
@{const List.upto} & @{typeof List.upto}\\ 

543 
@{const List.zip} & @{typeof List.zip}\\ 

544 
\end{supertabular} 

545 

546 
\subsubsection*{Syntax} 

547 

548 
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51489
diff
changeset

549 
@{text"[x\<^sub>1,\<dots>,x\<^sub>n]"} & @{text"x\<^sub>1 # \<dots> # x\<^sub>n # []"}\\ 
30293  550 
@{term"[m..<n]"} & @{term[source]"upt m n"}\\ 
551 
@{term"[i..j]"} & @{term[source]"upto i j"}\\ 

552 
@{text"[e. x \<leftarrow> xs]"} & @{term"map (%x. e) xs"}\\ 

553 
@{term"[x \<leftarrow> xs. b]"} & @{term[source]"filter (\<lambda>x. b) xs"} \\ 

554 
@{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\ 

555 
@{term"\<Sum>x\<leftarrow>xs. e"} & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\ 

556 
\end{supertabular} 

557 
\medskip 

558 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51489
diff
changeset

559 
List comprehension: @{text"[e. q\<^sub>1, \<dots>, q\<^sub>n]"} where each 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51489
diff
changeset

560 
qualifier @{text q\<^sub>i} is either a generator \mbox{@{text"pat \<leftarrow> e"}} or a 
30293  561 
guard, i.e.\ boolean expression. 
562 

50581  563 
\section*{Map} 
30293  564 

565 
Maps model partial functions and are often used as finite tables. However, 

566 
the domain of a map may be infinite. 

567 

568 
\begin{supertabular}{@ {} l @ {~::~} l @ {}} 

569 
@{const Map.empty} & @{typeof Map.empty}\\ 

570 
@{const Map.map_add} & @{typeof Map.map_add}\\ 

571 
@{const Map.map_comp} & @{typeof Map.map_comp}\\ 

572 
@{const Map.restrict_map} & @{term_type_only Map.restrict_map "('a\<Rightarrow>'b option)\<Rightarrow>'a set\<Rightarrow>('a\<Rightarrow>'b option)"}\\ 

573 
@{const Map.dom} & @{term_type_only Map.dom "('a\<Rightarrow>'b option)\<Rightarrow>'a set"}\\ 

574 
@{const Map.ran} & @{term_type_only Map.ran "('a\<Rightarrow>'b option)\<Rightarrow>'b set"}\\ 

575 
@{const Map.map_le} & @{typeof Map.map_le}\\ 

576 
@{const Map.map_of} & @{typeof Map.map_of}\\ 

577 
@{const Map.map_upds} & @{typeof Map.map_upds}\\ 

578 
\end{supertabular} 

579 

580 
\subsubsection*{Syntax} 

581 

582 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

30403  583 
@{term"Map.empty"} & @{term"\<lambda>x. None"}\\ 
30293  584 
@{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\ 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51489
diff
changeset

585 
@{text"m(x\<^sub>1\<mapsto>y\<^sub>1,\<dots>,x\<^sub>n\<mapsto>y\<^sub>n)"} & @{text[source]"m(x\<^sub>1\<mapsto>y\<^sub>1)\<dots>(x\<^sub>n\<mapsto>y\<^sub>n)"}\\ 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51489
diff
changeset

586 
@{text"[x\<^sub>1\<mapsto>y\<^sub>1,\<dots>,x\<^sub>n\<mapsto>y\<^sub>n]"} & @{text[source]"Map.empty(x\<^sub>1\<mapsto>y\<^sub>1,\<dots>,x\<^sub>n\<mapsto>y\<^sub>n)"}\\ 
30293  587 
@{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\ 
588 
\end{tabular} 

589 

50581  590 
\section*{Infix operators in Main} % @{theory Main} 
591 

592 
\begin{center} 

50605  593 
\begin{tabular}{llll} 
594 
& Operator & precedence & associativity \\ 

595 
\hline 

596 
Metalogic & @{text"\<Longrightarrow>"} & 1 & right \\ 

597 
& @{text"\<equiv>"} & 2 \\ 

598 
\hline 

599 
Logic & @{text"\<and>"} & 35 & right \\ 

600 
&@{text"\<or>"} & 30 & right \\ 

601 
&@{text"\<longrightarrow>"}, @{text"\<longleftrightarrow>"} & 25 & right\\ 

602 
&@{text"="}, @{text"\<noteq>"} & 50 & left\\ 

603 
\hline 

604 
Orderings & @{text"\<le>"}, @{text"<"}, @{text"\<ge>"}, @{text">"} & 50 \\ 

605 
\hline 

606 
Sets & @{text"\<subseteq>"}, @{text"\<subset>"}, @{text"\<supseteq>"}, @{text"\<supset>"} & 50 \\ 

607 
&@{text"\<in>"}, @{text"\<notin>"} & 50 \\ 

608 
&@{text"\<inter>"} & 70 & left \\ 

609 
&@{text"\<union>"} & 65 & left \\ 

610 
\hline 

611 
Functions and Relations & @{text"\<circ>"} & 55 & left\\ 

612 
&@{text"`"} & 90 & right\\ 

613 
&@{text"O"} & 75 & right\\ 

614 
&@{text"``"} & 90 & right\\ 

57570  615 
&@{text"^^"} & 80 & right\\ 
50605  616 
\hline 
617 
Numbers & @{text"+"}, @{text""} & 65 & left \\ 

618 
&@{text"*"}, @{text"/"} & 70 & left \\ 

619 
&@{text"div"}, @{text"mod"} & 70 & left\\ 

620 
&@{text"^"} & 80 & right\\ 

621 
&@{text"dvd"} & 50 \\ 

622 
\hline 

623 
Lists & @{text"#"}, @{text"@"} & 65 & right\\ 

624 
&@{text"!"} & 100 & left 

50581  625 
\end{tabular} 
626 
\end{center} 

30293  627 
*} 
628 
(*<*) 

629 
end 

630 
(*>*) 