doc-src/TutorialI/Misc/document/prime_def.tex
changeset 9145 9f7b8de5bfaf
parent 8749 2665170f104a
child 9458 c613cd06d5cf
--- a/doc-src/TutorialI/Misc/document/prime_def.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -9,3 +9,7 @@
 should have written is%
 \end{isamarkuptext}%
 ~{"}prime(p)~{\isasymequiv}~1~<~p~{\isasymand}~({\isasymforall}m.~(m~dvd~p)~{\isasymlongrightarrow}~(m=1~{\isasymor}~m=p)){"}\end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: