equal
deleted
inserted
replaced
161 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
161 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
162 @{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\ |
162 @{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\ |
163 @{text"f(x\<^isub>1:=y\<^isub>1,\<dots>,x\<^isub>n:=y\<^isub>n)"} & @{text"f(x\<^isub>1:=y\<^isub>1)\<dots>(x\<^isub>n:=y\<^isub>n)"}\\ |
163 @{text"f(x\<^isub>1:=y\<^isub>1,\<dots>,x\<^isub>n:=y\<^isub>n)"} & @{text"f(x\<^isub>1:=y\<^isub>1)\<dots>(x\<^isub>n:=y\<^isub>n)"}\\ |
164 \end{tabular} |
164 \end{tabular} |
165 |
165 |
|
166 |
|
167 \section{Hilbert\_Choice} |
|
168 |
|
169 Hilbert's selection ($\varepsilon$) operator: @{term"SOME x. P"}. |
|
170 \smallskip |
|
171 |
|
172 \begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
173 @{const Hilbert_Choice.inv_onto} & @{term_type_only Hilbert_Choice.inv_onto "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"} |
|
174 \end{tabular} |
|
175 |
|
176 \subsubsection*{Syntax} |
|
177 |
|
178 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
179 @{term inv} & @{term[source]"inv_onto UNIV"} |
|
180 \end{tabular} |
166 |
181 |
167 \section{Fixed Points} |
182 \section{Fixed Points} |
168 |
183 |
169 Theory: @{theory Inductive}. |
184 Theory: @{theory Inductive}. |
170 |
185 |