diff -r 0c86acc069ad -r 5deda0549f97 doc-src/TutorialI/Misc/document/prime_def.tex
--- a/doc-src/TutorialI/Misc/document/prime_def.tex	Thu Jul 26 16:54:44 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{prime{\isaliteral{5F}{\isacharunderscore}}def}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\begin{isamarkuptext}%
-\begin{warn}
-A common mistake when writing definitions is to introduce extra free
-variables on the right-hand side.  Consider the following, flawed definition
-(where \isa{dvd} means ``divides''):
-\begin{isabelle}%
-\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}prime\ p\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ p\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}m\ dvd\ p\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ m\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ m\ {\isaliteral{3D}{\isacharequal}}\ p{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}%
-\end{isabelle}
-\par\noindent\hangindent=0pt
-Isabelle rejects this ``definition'' because of the extra \isa{m} on the
-right-hand side, which would introduce an inconsistency (why?). 
-The correct version is
-\begin{isabelle}%
-\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}prime\ p\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ p\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{2E}{\isachardot}}\ m\ dvd\ p\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ m\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ m\ {\isaliteral{3D}{\isacharequal}}\ p{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}%
-\end{isabelle}
-\end{warn}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: