--- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Wed Oct 24 21:12:44 2007 +0200
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Wed Oct 24 21:33:37 2007 +0200
@@ -1303,7 +1303,7 @@
\ findzero{\isachardot}domintros%
\begin{isamarkuptext}%
\begin{isabelle}%
-{\isacharparenleft}{\isacharquery}f\ {\isacharquery}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}%
+{\isacharparenleft}{\isadigit{0}}\ {\isacharless}\ {\isacharquery}f\ {\isacharquery}n\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}%
\end{isabelle}
Domain introduction rules allow to show that a given value lies in the