diff -r c7b2f68c79fb -r ce86227f29d0 etc/settings
--- a/etc/settings	Thu Oct 07 12:27:44 1999 +0200
+++ b/etc/settings	Thu Oct 07 12:33:54 1999 +0200
@@ -52,6 +52,20 @@
 
 
 ###
+### Document preparation
+###
+
+#TeX environment hacking (for teTeX)
+unset TEXMF
+PATH="/usr/local/tetex-1.0/bin:$PATH"
+
+TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS"
+ISABELLE_LATEX="latex"
+ISABELLE_PDFLATEX="pdflatex"
+ISABELLE_DVIPS="dvips -D 600"
+
+
+###
 ### Misc path settings
 ###