author nipkow Mon Dec 17 18:23:08 2012 +0100 (2012-12-17) changeset 50581 0eaefd4306d7 parent 50580 fbb973a53106 child 50582 001a0e12d7f1
     1.1 --- a/src/Doc/Main/Main_Doc.thy	Mon Dec 17 17:19:21 2012 +0100
1.2 +++ b/src/Doc/Main/Main_Doc.thy	Mon Dec 17 18:23:08 2012 +0100
1.3 @@ -26,10 +26,10 @@
1.4  text{*
1.5
1.6  \begin{abstract}
1.7 -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. The sophisticated class structure is only hinted at. For details see \url{http://isabelle.in.tum.de/library/HOL/}.
1.8 +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/}.
1.9  \end{abstract}
1.10
1.11 -\section{HOL}
1.12 +\section*{HOL}
1.13
1.14  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"}.
1.15  \smallskip
1.16 @@ -49,7 +49,7 @@
1.17  \end{supertabular}
1.18
1.19
1.20 -\section{Orderings}
1.21 +\section*{Orderings}
1.22
1.23  A collection of classes defining basic orderings:
1.24  preorder, partial order, linear order, dense linear order and wellorder.
1.25 @@ -79,7 +79,7 @@
1.26  \end{supertabular}
1.27
1.28
1.29 -\section{Lattices}
1.30 +\section*{Lattices}
1.31
1.32  Classes semilattice, lattice, distributive lattice and complete lattice (the
1.33  latter in theory @{theory Set}).
1.34 @@ -108,10 +108,7 @@
1.35  \end{supertabular}
1.36
1.37
1.38 -\section{Set}
1.39 -
1.40 -%Sets are predicates: @{text[source]"'a set  =  'a \<Rightarrow> bool"}
1.41 -%\bigskip
1.42 +\section*{Set}
1.43
1.44  \begin{supertabular}{@ {} l @ {~::~} l l @ {}}
1.45  @{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\
1.46 @@ -151,7 +148,7 @@
1.47  \end{supertabular}
1.48
1.49
1.50 -\section{Fun}
1.51 +\section*{Fun}
1.52
1.53  \begin{supertabular}{@ {} l @ {~::~} l l @ {}}
1.54  @{const "Fun.id"} & @{typeof Fun.id}\\
1.55 @@ -172,7 +169,7 @@
1.56  \end{tabular}
1.57
1.58
1.59 -\section{Hilbert\_Choice}
1.60 +\section*{Hilbert\_Choice}
1.61
1.62  Hilbert's selection ($\varepsilon$) operator: @{term"SOME x. P"}.
1.63  \smallskip
1.64 @@ -187,7 +184,7 @@
1.65  @{term inv} & @{term[source]"inv_into UNIV"}
1.66  \end{tabular}
1.67
1.68 -\section{Fixed Points}
1.69 +\section*{Fixed Points}
1.70
1.71  Theory: @{theory Inductive}.
1.72
1.73 @@ -200,7 +197,7 @@
1.74
1.75  Note that in particular sets (@{typ"'a \<Rightarrow> bool"}) are complete lattices.
1.76
1.77 -\section{Sum\_Type}
1.78 +\section*{Sum\_Type}
1.79
1.80  Type constructor @{text"+"}.
1.81
1.82 @@ -211,7 +208,7 @@
1.83  \end{tabular}
1.84
1.85
1.86 -\section{Product\_Type}
1.87 +\section*{Product\_Type}
1.88
1.89  Types @{typ unit} and @{text"\<times>"}.
1.90
1.91 @@ -239,7 +236,7 @@
1.92  e.g.\ \mbox{@{prop"ALL (x,y):A. P"},} @{term"{(x,y). P}"}, etc.
1.93
1.94
1.95 -\section{Relation}
1.96 +\section*{Relation}
1.97
1.98  \begin{tabular}{@ {} l @ {~::~} l @ {}}
1.99  @{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\
1.100 @@ -271,7 +268,7 @@
1.101  \noindent
1.102  Type synonym \ @{typ"'a rel"} @{text"="} @{expanded_typ "'a rel"}
1.103
1.104 -\section{Equiv\_Relations}
1.105 +\section*{Equiv\_Relations}
1.106
1.107  \begin{supertabular}{@ {} l @ {~::~} l @ {}}
1.108  @{const Equiv_Relations.equiv} & @{term_type_only Equiv_Relations.equiv "'a set \<Rightarrow> ('a*'a)set\<Rightarrow>bool"}\\
1.109 @@ -289,7 +286,7 @@
1.110  \end{tabular}
1.111
1.112
1.113 -\section{Transitive\_Closure}
1.114 +\section*{Transitive\_Closure}
1.115
1.116  \begin{tabular}{@ {} l @ {~::~} l @ {}}
1.117  @{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
1.118 @@ -308,7 +305,7 @@
1.119  \end{tabular}
1.120
1.121
1.122 -\section{Algebra}
1.123 +\section*{Algebra}
1.124
1.125  Theories @{theory Groups}, @{theory Rings}, @{theory Fields} and @{theory
1.126  Divides} define a large collection of classes describing common algebraic
1.127 @@ -338,7 +335,7 @@
1.128  \end{tabular}
1.129
1.130
1.131 -\section{Nat}
1.132 +\section*{Nat}
1.133
1.134  @{datatype nat}
1.135  \bigskip
1.136 @@ -365,7 +362,7 @@
1.137    @{term_type_only "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"}
1.138  \end{tabular}
1.139
1.140 -\section{Int}
1.141 +\section*{Int}
1.142
1.143  Type @{typ int}
1.144  \bigskip
1.145 @@ -402,7 +399,7 @@
1.146  \end{tabular}
1.147
1.148
1.149 -\section{Finite\_Set}
1.150 +\section*{Finite\_Set}
1.151
1.152
1.153  \begin{supertabular}{@ {} l @ {~::~} l @ {}}
1.154 @@ -425,7 +422,7 @@
1.155  \end{supertabular}
1.156
1.157
1.158 -\section{Wellfounded}
1.159 +\section*{Wellfounded}
1.160
1.161  \begin{supertabular}{@ {} l @ {~::~} l @ {}}
1.162  @{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\<Rightarrow>bool"}\\
1.163 @@ -438,7 +435,7 @@
1.164  \end{supertabular}
1.165
1.166
1.167 -\section{SetInterval}
1.168 +\section*{Set\_Interval} % @{theory Set_Interval}
1.169
1.170  \begin{supertabular}{@ {} l @ {~::~} l @ {}}
1.171  @{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\
1.172 @@ -473,14 +470,14 @@
1.173  \end{supertabular}
1.174
1.175
1.176 -\section{Power}
1.177 +\section*{Power}
1.178
1.179  \begin{tabular}{@ {} l @ {~::~} l @ {}}
1.180  @{const Power.power} & @{typeof Power.power}
1.181  \end{tabular}
1.182
1.183
1.184 -\section{Option}
1.185 +\section*{Option}
1.186
1.187  @{datatype option}
1.188  \bigskip
1.189 @@ -492,7 +489,7 @@
1.190  @{const Option.bind} & @{term_type_only Option.bind "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"}
1.191  \end{tabular}
1.192
1.193 -\section{List}
1.194 +\section*{List}
1.195
1.196  @{datatype list}
1.197  \bigskip
1.198 @@ -563,7 +560,7 @@
1.199  qualifier @{text q\<^isub>i} is either a generator \mbox{@{text"pat \<leftarrow> e"}} or a
1.200  guard, i.e.\ boolean expression.
1.201
1.202 -\section{Map}
1.203 +\section*{Map}
1.204
1.205  Maps model partial functions and are often used as finite tables. However,
1.206  the domain of a map may be infinite.
1.207 @@ -590,6 +587,35 @@
1.208  @{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\
1.209  \end{tabular}
1.210
1.211 +\section*{Infix operators in Main} % @{theory Main}
1.212 +
1.213 +\begin{center}
1.214 +\begin{tabular}{lll}
1.215 +Operator & precedence & associativity \\
1.216 +@{text"="}, @{text"\<noteq>"} & 50 & left\\
1.217 +@{text"\<le>"}, @{text"<"}, @{text"\<ge>"}, @{text">"} & 50 \\
1.218 +@{text"\<and>"} & 35 & right \\
1.219 +@{text"\<or>"} & 30 & right \\
1.220 +@{text"\<longrightarrow>"}, @{text"\<longleftrightarrow>"} & 25 & right\\
1.221 +@{text"\<subseteq>"}, @{text"\<subset>"}, @{text"\<supseteq>"}, @{text"\<supset>"} & 50 \\
1.222 +@{text"\<in>"}, @{text"\<notin>"} & 50 \\
1.223 +@{text"\<inter>"} & 70 & left \\
1.224 +@{text"\<union>"} & 65 & left \\
1.225 +@{text"\<circ>"} & 55 & left\\
1.226 +@{text""} & 90 & right\\
1.227 +@{text"O"} & 75 & right\\
1.228 +@{text""} & 90 & right\\
1.229 +@{text"+"}, @{text"-"} & 65 & left \\
1.230 +@{text"*"}, @{text"/"} & 70 & left \\
1.231 +@{text"div"}, @{text"mod"} & 70 & left\\
1.232 +@{text"^"} & 80 & right\\
1.233 +@{text"^^"} & 80 & right\\
1.234 +@{text"dvd"} & 50 \\
1.235 +@{text"#"}, @{text"@"} & 65 & right\\
1.236 +@{text"!"} & 100 & left\\
1.237 +@{text"++"} & 100 & left\\
1.238 +\end{tabular}
1.239 +\end{center}
1.240  *}
1.241  (*<*)
1.242  end
`