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