| 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: