# HG changeset patch
# User wenzelm
# Date 962011309 -7200
# Node ID 9f7b8de5bfaf47e7d503826f2ef79b15f3d8583c
# Parent  20a70ef9c32043936a79760277935470e000d092
updated;

diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/AxClass/generated/Group.tex
--- a/doc-src/AxClass/generated/Group.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/AxClass/generated/Group.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -294,3 +294,7 @@
  theories.%
 \end{isamarkuptext}%
 \isacommand{end}\end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/AxClass/generated/NatClass.tex
--- a/doc-src/AxClass/generated/NatClass.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/AxClass/generated/NatClass.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -56,3 +56,7 @@
  constraints).%
 \end{isamarkuptext}%
 \isacommand{end}\end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/AxClass/generated/Product.tex
--- a/doc-src/AxClass/generated/Product.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/AxClass/generated/Product.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -75,3 +75,7 @@
  operations'' or even ``names of functions''.%
 \end{isamarkuptext}%
 \isacommand{end}\end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/AxClass/generated/Semigroups.tex
--- a/doc-src/AxClass/generated/Semigroups.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/AxClass/generated/Semigroups.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -47,3 +47,7 @@
  same.%
 \end{isamarkuptext}%
 \isacommand{end}\end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/CodeGen/document/CodeGen.tex
--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -112,3 +112,7 @@
 its instance.%
 \end{isamarkuptext}%
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Datatype/document/ABexpr.tex
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -112,3 +112,7 @@
 \end{exercise}%
 \end{isamarkuptext}%
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Datatype/document/Fundata.tex
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -46,3 +46,7 @@
 \end{isabellepar}%%
 \end{isamarkuptext}%
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Datatype/document/Nested.tex
--- a/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -81,3 +81,7 @@
 expressions as its argument: \isa{Sum "'a aexp list"}.%
 \end{isamarkuptext}%
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Datatype/document/unfoldnested.tex
--- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -1,3 +1,7 @@
 \begin{isabelle}%
 \isacommand{datatype}~('a,'b){"}term{"}~=~Var~'a~|~App~'b~{"}('a,'b)term\_list{"}\isanewline
 \isakeyword{and}~('a,'b)term\_list~=~Nil~|~Cons~{"}('a,'b)term{"}~{"}('a,'b)term\_list{"}\end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -132,3 +132,7 @@
 normality of \isa{normif}:%
 \end{isamarkuptext}%
 \isacommand{lemma}~[simp]:~{"}{\isasymforall}t~e.~normal(normif~b~t~e)~=~(normal~t~{\isasymand}~normal~e){"}\end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/Itrev.tex
--- a/doc-src/TutorialI/Misc/document/Itrev.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -77,3 +77,7 @@
 applied blindly.%
 \end{isamarkuptxt}%
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/Tree.tex
--- a/doc-src/TutorialI/Misc/document/Tree.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -11,3 +11,7 @@
 by swapping subtrees (recursively). Prove%
 \end{isamarkuptext}%
 \isacommand{lemma}~mirror\_mirror:~{"}mirror(mirror~t)~=~t{"}\end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/arith1.tex
--- a/doc-src/TutorialI/Misc/document/arith1.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith1.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -1,3 +1,7 @@
 \begin{isabelle}%
 \isacommand{lemma}~{"}{\isasymlbrakk}~{\isasymnot}~m~<~n;~m~<~n+1~{\isasymrbrakk}~{\isasymLongrightarrow}~m~=~n{"}\isanewline
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/arith2.tex
--- a/doc-src/TutorialI/Misc/document/arith2.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith2.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -2,3 +2,7 @@
 \isacommand{lemma}~{"}min~i~(max~j~(k*k))~=~max~(min~(k*k)~i)~(min~i~(j::nat)){"}\isanewline
 \isacommand{apply}(arith)\isacommand{.}\isanewline
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/arith3.tex
--- a/doc-src/TutorialI/Misc/document/arith3.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith3.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -1,3 +1,7 @@
 \begin{isabelle}%
 \isacommand{lemma}~{"}n*n~=~n~{\isasymLongrightarrow}~n=0~{\isasymor}~n=1{"}\isanewline
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/arith4.tex
--- a/doc-src/TutorialI/Misc/document/arith4.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith4.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -1,3 +1,7 @@
 \begin{isabelle}%
 \isacommand{lemma}~{"}{\isasymnot}~m~<~n~{\isasymand}~m~<~n+1~{\isasymLongrightarrow}~m~=~n{"}\isanewline
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/asm_simp.tex
--- a/doc-src/TutorialI/Misc/document/asm_simp.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/asm_simp.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -43,3 +43,7 @@
 other arguments.%
 \end{isamarkuptext}%
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/case_splits.tex
--- a/doc-src/TutorialI/Misc/document/case_splits.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/case_splits.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -65,3 +65,7 @@
 \end{isamarkuptext}%
 \isacommand{theorems}~[split~del]~=~list.split\isanewline
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/cases.tex
--- a/doc-src/TutorialI/Misc/document/cases.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cases.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -13,3 +13,7 @@
 \end{isamarkuptxt}%
 \isacommand{apply}(auto)\isacommand{.}\isanewline
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/cond_rewr.tex
--- a/doc-src/TutorialI/Misc/document/cond_rewr.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -27,3 +27,7 @@
 assumption of the subgoal.%
 \end{isamarkuptext}%
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/def_rewr.tex
--- a/doc-src/TutorialI/Misc/document/def_rewr.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/def_rewr.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -42,3 +42,7 @@
 rule because this defeats the whole purpose of an abbreviation.%
 \end{isamarkuptext}%
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/fakenat.tex
--- a/doc-src/TutorialI/Misc/document/fakenat.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/fakenat.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -6,3 +6,7 @@
 behaves like%
 \end{isamarkuptext}%
 \isacommand{datatype}~nat~=~{"}0{"}~|~Suc~nat\end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/let_rewr.tex
--- a/doc-src/TutorialI/Misc/document/let_rewr.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/let_rewr.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -6,3 +6,7 @@
 of nested \isa{let}s one could even add \isa{Let_def} permanently:%
 \end{isamarkuptext}%
 \isacommand{theorems}~[simp]~=~Let\_def\end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -20,3 +20,7 @@
 \isacommand{apply}(induct\_tac~n)\isanewline
 \isacommand{apply}(auto)\isacommand{.}\isanewline
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/pairs.tex
--- a/doc-src/TutorialI/Misc/document/pairs.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/pairs.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -1,3 +1,7 @@
 \begin{isabelle}%
 ~{"}let~(x,y)~=~f~z~in~(y,x){"}~{"}case~xs~of~[]~{\isasymRightarrow}~0~|~(x,y)\#zs~{\isasymRightarrow}~x+y{"}\isanewline
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/prime_def.tex
--- 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:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/trace_simp.tex
--- a/doc-src/TutorialI/Misc/document/trace_simp.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/trace_simp.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -37,3 +37,7 @@
 \end{isamarkuptxt}%
 \isacommand{ML}~{"}reset~trace\_simp{"}\isanewline
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Misc/document/types.tex
--- a/doc-src/TutorialI/Misc/document/types.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/types.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -39,3 +39,7 @@
 $f$ is the name of the defined constant.%
 \end{isamarkuptext}%
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Recdef/document/Induction.tex
--- a/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -63,3 +63,7 @@
 (in which case you may assume it holds for the tail of that list).%
 \end{isamarkuptext}%
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Recdef/document/examples.tex
--- a/doc-src/TutorialI/Recdef/document/examples.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/examples.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -78,3 +78,7 @@
 set \isa{\{\}}.%
 \end{isamarkuptext}%
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Recdef/document/simplification.tex
--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -88,3 +88,7 @@
 \end{isamarkuptext}%
 \isacommand{lemmas}~[simp~del]~=~gcd.simps\isanewline
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Recdef/document/termination.tex
--- a/doc-src/TutorialI/Recdef/document/termination.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -87,3 +87,7 @@
 library.%
 \end{isamarkuptext}%
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -323,3 +323,7 @@
 \end{isamarkuptext}%
 \isacommand{end}\isanewline
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Trie/document/Option2.tex
--- a/doc-src/TutorialI/Trie/document/Option2.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Option2.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -1,3 +1,7 @@
 \begin{isabelle}%
 \isanewline
 \isacommand{datatype}~'a~option~=~None~|~Some~'a\end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r 20a70ef9c320 -r 9f7b8de5bfaf doc-src/TutorialI/Trie/document/Trie.tex
--- a/doc-src/TutorialI/Trie/document/Trie.tex	Mon Jun 26 00:23:17 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex	Mon Jun 26 11:21:49 2000 +0200
@@ -124,3 +124,7 @@
 proofs.%
 \end{isamarkuptext}%
 \end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: