10267
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{CTLind}%
|
17056
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
|
10 |
%
|
|
11 |
\endisatagtheory
|
|
12 |
{\isafoldtheory}%
|
|
13 |
%
|
|
14 |
\isadelimtheory
|
|
15 |
%
|
|
16 |
\endisadelimtheory
|
10267
|
17 |
%
|
10878
|
18 |
\isamarkupsubsection{CTL Revisited%
|
10395
|
19 |
}
|
11866
|
20 |
\isamarkuptrue%
|
10267
|
21 |
%
|
|
22 |
\begin{isamarkuptext}%
|
|
23 |
\label{sec:CTL-revisited}
|
11494
|
24 |
\index{CTL|(}%
|
|
25 |
The purpose of this section is twofold: to demonstrate
|
|
26 |
some of the induction principles and heuristics discussed above and to
|
10283
|
27 |
show how inductive definitions can simplify proofs.
|
10267
|
28 |
In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
|
10795
|
29 |
model checker for CTL\@. In particular the proof of the
|
10267
|
30 |
\isa{infinity{\isacharunderscore}lemma} on the way to \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} is not as
|
11494
|
31 |
simple as one might expect, due to the \isa{SOME} operator
|
10283
|
32 |
involved. Below we give a simpler proof of \isa{AF{\isacharunderscore}lemma{\isadigit{2}}}
|
|
33 |
based on an auxiliary inductive definition.
|
10267
|
34 |
|
|
35 |
Let us call a (finite or infinite) path \emph{\isa{A}-avoiding} if it does
|
|
36 |
not touch any node in the set \isa{A}. Then \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} says
|
|
37 |
that if no infinite path from some state \isa{s} is \isa{A}-avoiding,
|
|
38 |
then \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. We prove this by inductively defining the set
|
|
39 |
\isa{Avoid\ s\ A} of states reachable from \isa{s} by a finite \isa{A}-avoiding path:
|
|
40 |
% Second proof of opposite direction, directly by well-founded induction
|
|
41 |
% on the initial segment of M that avoids A.%
|
|
42 |
\end{isamarkuptext}%
|
17175
|
43 |
\isamarkuptrue%
|
|
44 |
\isacommand{consts}\isamarkupfalse%
|
|
45 |
\ Avoid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequoteclose}\isanewline
|
|
46 |
\isacommand{inductive}\isamarkupfalse%
|
|
47 |
\ {\isachardoublequoteopen}Avoid\ s\ A{\isachardoublequoteclose}\isanewline
|
|
48 |
\isakeyword{intros}\ {\isachardoublequoteopen}s\ {\isasymin}\ Avoid\ s\ A{\isachardoublequoteclose}\isanewline
|
|
49 |
\ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}\ t\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\ t\ {\isasymnotin}\ A{\isacharsemicolon}\ {\isacharparenleft}t{\isacharcomma}u{\isacharparenright}\ {\isasymin}\ M\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ u\ {\isasymin}\ Avoid\ s\ A{\isachardoublequoteclose}%
|
10267
|
50 |
\begin{isamarkuptext}%
|
|
51 |
It is easy to see that for any infinite \isa{A}-avoiding path \isa{f}
|
12492
|
52 |
with \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path
|
10267
|
53 |
starting with \isa{s} because (by definition of \isa{Avoid}) there is a
|
12492
|
54 |
finite \isa{A}-avoiding path from \isa{s} to \isa{f\ {\isadigit{0}}}.
|
|
55 |
The proof is by induction on \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A}. However,
|
10267
|
56 |
this requires the following
|
|
57 |
reformulation, as explained in \S\ref{sec:ind-var-in-prems} above;
|
|
58 |
the \isa{rule{\isacharunderscore}format} directive undoes the reformulation after the proof.%
|
|
59 |
\end{isamarkuptext}%
|
17175
|
60 |
\isamarkuptrue%
|
|
61 |
\isacommand{lemma}\isamarkupfalse%
|
|
62 |
\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
|
|
63 |
\ \ {\isachardoublequoteopen}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline
|
|
64 |
\ \ \ {\isasymforall}f{\isasymin}Paths\ t{\isachardot}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ f\ i\ {\isasymnotin}\ A{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
17056
|
65 |
%
|
|
66 |
\isadelimproof
|
|
67 |
%
|
|
68 |
\endisadelimproof
|
|
69 |
%
|
|
70 |
\isatagproof
|
17175
|
71 |
\isacommand{apply}\isamarkupfalse%
|
|
72 |
{\isacharparenleft}erule\ Avoid{\isachardot}induct{\isacharparenright}\isanewline
|
|
73 |
\ \isacommand{apply}\isamarkupfalse%
|
|
74 |
{\isacharparenleft}blast{\isacharparenright}\isanewline
|
|
75 |
\isacommand{apply}\isamarkupfalse%
|
|
76 |
{\isacharparenleft}clarify{\isacharparenright}\isanewline
|
|
77 |
\isacommand{apply}\isamarkupfalse%
|
|
78 |
{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}i{\isachardot}\ case\ i\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ t\ {\isacharbar}\ Suc\ i\ {\isasymRightarrow}\ f\ i{\isachardoublequoteclose}\ \isakeyword{in}\ bspec{\isacharparenright}\isanewline
|
|
79 |
\isacommand{apply}\isamarkupfalse%
|
|
80 |
{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Paths{\isacharunderscore}def\ split{\isacharcolon}\ nat{\isachardot}split{\isacharparenright}\isanewline
|
|
81 |
\isacommand{done}\isamarkupfalse%
|
|
82 |
%
|
17056
|
83 |
\endisatagproof
|
|
84 |
{\isafoldproof}%
|
|
85 |
%
|
|
86 |
\isadelimproof
|
|
87 |
%
|
|
88 |
\endisadelimproof
|
11866
|
89 |
%
|
10267
|
90 |
\begin{isamarkuptext}%
|
|
91 |
\noindent
|
11494
|
92 |
The base case (\isa{t\ {\isacharequal}\ s}) is trivial and proved by \isa{blast}.
|
10267
|
93 |
In the induction step, we have an infinite \isa{A}-avoiding path \isa{f}
|
|
94 |
starting from \isa{u}, a successor of \isa{t}. Now we simply instantiate
|
|
95 |
the \isa{{\isasymforall}f{\isasymin}Paths\ t} in the induction hypothesis by the path starting with
|
|
96 |
\isa{t} and continuing with \isa{f}. That is what the above $\lambda$-term
|
10878
|
97 |
expresses. Simplification shows that this is a path starting with \isa{t}
|
|
98 |
and that the instantiated induction hypothesis implies the conclusion.
|
10267
|
99 |
|
11196
|
100 |
Now we come to the key lemma. Assuming that no infinite \isa{A}-avoiding
|
11277
|
101 |
path starts from \isa{s}, we want to show \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. For the
|
|
102 |
inductive proof this must be generalized to the statement that every point \isa{t}
|
11494
|
103 |
``between'' \isa{s} and \isa{A}, in other words all of \isa{Avoid\ s\ A},
|
11196
|
104 |
is contained in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}:%
|
10267
|
105 |
\end{isamarkuptext}%
|
17175
|
106 |
\isamarkuptrue%
|
|
107 |
\isacommand{lemma}\isamarkupfalse%
|
|
108 |
\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline
|
|
109 |
\ \ {\isachardoublequoteopen}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ t\ {\isasymin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequoteclose}%
|
17056
|
110 |
\isadelimproof
|
|
111 |
%
|
|
112 |
\endisadelimproof
|
|
113 |
%
|
|
114 |
\isatagproof
|
16069
|
115 |
%
|
|
116 |
\begin{isamarkuptxt}%
|
|
117 |
\noindent
|
|
118 |
The proof is by induction on the ``distance'' between \isa{t} and \isa{A}. Remember that \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}.
|
|
119 |
If \isa{t} is already in \isa{A}, then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} is
|
|
120 |
trivial. If \isa{t} is not in \isa{A} but all successors are in
|
|
121 |
\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}} (induction hypothesis), then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} is
|
|
122 |
again trivial.
|
|
123 |
|
|
124 |
The formal counterpart of this proof sketch is a well-founded induction
|
|
125 |
on~\isa{M} restricted to \isa{Avoid\ s\ A\ {\isacharminus}\ A}, roughly speaking:
|
|
126 |
\begin{isabelle}%
|
|
127 |
\ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}%
|
|
128 |
\end{isabelle}
|
|
129 |
As we shall see presently, the absence of infinite \isa{A}-avoiding paths
|
|
130 |
starting from \isa{s} implies well-foundedness of this relation. For the
|
|
131 |
moment we assume this and proceed with the induction:%
|
|
132 |
\end{isamarkuptxt}%
|
17175
|
133 |
\isamarkuptrue%
|
|
134 |
\isacommand{apply}\isamarkupfalse%
|
|
135 |
{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequoteopen}wf{\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
|
|
136 |
\ \isacommand{apply}\isamarkupfalse%
|
|
137 |
{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline
|
|
138 |
\ \isacommand{apply}\isamarkupfalse%
|
17181
|
139 |
{\isacharparenleft}clarsimp{\isacharparenright}%
|
16069
|
140 |
\begin{isamarkuptxt}%
|
|
141 |
\noindent
|
|
142 |
\begin{isabelle}%
|
|
143 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\isanewline
|
|
144 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ }{\isasymforall}y{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline
|
|
145 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ {\isasymforall}y{\isachardot}\ }y\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ y\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline
|
|
146 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ }t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\isanewline
|
|
147 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ }{\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
|
|
148 |
\ {\isadigit{2}}{\isachardot}\ {\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\isanewline
|
|
149 |
\isaindent{\ {\isadigit{2}}{\isachardot}\ }wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}%
|
|
150 |
\end{isabelle}
|
|
151 |
Now the induction hypothesis states that if \isa{t\ {\isasymnotin}\ A}
|
|
152 |
then all successors of \isa{t} that are in \isa{Avoid\ s\ A} are in
|
|
153 |
\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Unfolding \isa{lfp} in the conclusion of the first
|
|
154 |
subgoal once, we have to prove that \isa{t} is in \isa{A} or all successors
|
|
155 |
of \isa{t} are in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. But if \isa{t} is not in \isa{A},
|
|
156 |
the second
|
|
157 |
\isa{Avoid}-rule implies that all successors of \isa{t} are in
|
|
158 |
\isa{Avoid\ s\ A}, because we also assume \isa{t\ {\isasymin}\ Avoid\ s\ A}.
|
|
159 |
Hence, by the induction hypothesis, all successors of \isa{t} are indeed in
|
|
160 |
\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Mechanically:%
|
|
161 |
\end{isamarkuptxt}%
|
17175
|
162 |
\isamarkuptrue%
|
|
163 |
\ \isacommand{apply}\isamarkupfalse%
|
|
164 |
{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
|
|
165 |
\ \isacommand{apply}\isamarkupfalse%
|
|
166 |
{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
|
|
167 |
\ \isacommand{apply}\isamarkupfalse%
|
|
168 |
{\isacharparenleft}blast\ intro{\isacharcolon}\ Avoid{\isachardot}intros{\isacharparenright}%
|
16069
|
169 |
\begin{isamarkuptxt}%
|
|
170 |
Having proved the main goal, we return to the proof obligation that the
|
|
171 |
relation used above is indeed well-founded. This is proved by contradiction: if
|
|
172 |
the relation is not well-founded then there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem
|
|
173 |
\isa{wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain}:
|
|
174 |
\begin{isabelle}%
|
|
175 |
\ \ \ \ \ wf\ r\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ {\isacharparenleft}{\isasymexists}f{\isachardot}\ {\isasymforall}i{\isachardot}\ {\isacharparenleft}f\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharcomma}\ f\ i{\isacharparenright}\ {\isasymin}\ r{\isacharparenright}{\isacharparenright}%
|
|
176 |
\end{isabelle}
|
|
177 |
From lemma \isa{ex{\isacharunderscore}infinite{\isacharunderscore}path} the existence of an infinite
|
|
178 |
\isa{A}-avoiding path starting in \isa{s} follows, contradiction.%
|
|
179 |
\end{isamarkuptxt}%
|
17175
|
180 |
\isamarkuptrue%
|
|
181 |
\isacommand{apply}\isamarkupfalse%
|
|
182 |
{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline
|
|
183 |
\isacommand{apply}\isamarkupfalse%
|
|
184 |
{\isacharparenleft}simp\ add{\isacharcolon}\ wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline
|
|
185 |
\isacommand{apply}\isamarkupfalse%
|
|
186 |
{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
|
|
187 |
\isacommand{apply}\isamarkupfalse%
|
|
188 |
{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline
|
|
189 |
\isacommand{apply}\isamarkupfalse%
|
|
190 |
{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Paths{\isacharunderscore}def{\isacharparenright}\isanewline
|
|
191 |
\isacommand{done}\isamarkupfalse%
|
|
192 |
%
|
17056
|
193 |
\endisatagproof
|
|
194 |
{\isafoldproof}%
|
|
195 |
%
|
|
196 |
\isadelimproof
|
|
197 |
%
|
|
198 |
\endisadelimproof
|
11866
|
199 |
%
|
10267
|
200 |
\begin{isamarkuptext}%
|
11196
|
201 |
The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive in the
|
|
202 |
statement of the lemma means
|
11494
|
203 |
that the assumption is left unchanged; otherwise the \isa{{\isasymforall}p}
|
|
204 |
would be turned
|
10267
|
205 |
into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is,
|
|
206 |
\isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now
|
|
207 |
\begin{isabelle}%
|
10696
|
208 |
\ \ \ \ \ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}%
|
10267
|
209 |
\end{isabelle}
|
|
210 |
The main theorem is simply the corollary where \isa{t\ {\isacharequal}\ s},
|
11494
|
211 |
when the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true
|
10845
|
212 |
by the first \isa{Avoid}-rule. Isabelle confirms this:%
|
11494
|
213 |
\index{CTL|)}%
|
10267
|
214 |
\end{isamarkuptext}%
|
17175
|
215 |
\isamarkuptrue%
|
|
216 |
\isacommand{theorem}\isamarkupfalse%
|
|
217 |
\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
17056
|
218 |
%
|
|
219 |
\isadelimproof
|
|
220 |
%
|
|
221 |
\endisadelimproof
|
|
222 |
%
|
|
223 |
\isatagproof
|
17175
|
224 |
\isacommand{by}\isamarkupfalse%
|
|
225 |
{\isacharparenleft}auto\ elim{\isacharcolon}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}\ Avoid{\isachardot}intros{\isacharparenright}\isanewline
|
15488
|
226 |
\isanewline
|
17056
|
227 |
%
|
|
228 |
\endisatagproof
|
|
229 |
{\isafoldproof}%
|
|
230 |
%
|
|
231 |
\isadelimproof
|
|
232 |
%
|
|
233 |
\endisadelimproof
|
|
234 |
%
|
|
235 |
\isadelimtheory
|
|
236 |
%
|
|
237 |
\endisadelimtheory
|
|
238 |
%
|
|
239 |
\isatagtheory
|
|
240 |
%
|
|
241 |
\endisatagtheory
|
|
242 |
{\isafoldtheory}%
|
|
243 |
%
|
|
244 |
\isadelimtheory
|
|
245 |
%
|
|
246 |
\endisadelimtheory
|
10267
|
247 |
\end{isabellebody}%
|
|
248 |
%%% Local Variables:
|
|
249 |
%%% mode: latex
|
|
250 |
%%% TeX-master: "root"
|
|
251 |
%%% End:
|