author | paulson |
Fri, 18 Mar 2005 14:31:50 +0100 | |
changeset 15614 | b098158a3f39 |
parent 15481 | fc075ae929e4 |
child 16069 | 3f2a9f400168 |
permissions | -rw-r--r-- |
10365 | 1 |
% |
11187 | 2 |
\begin{isabellebody}% |
3 |
\def\isabellecontext{Advanced}% |
|
10365 | 4 |
\isanewline |
11187 | 5 |
\isacommand{theory}\ Advanced\ {\isacharequal}\ Even{\isacharcolon}\isanewline |
10469 | 6 |
\isanewline |
7 |
\isanewline |
|
11866 | 8 |
\isamarkupfalse% |
11187 | 9 |
\isacommand{datatype}\ {\isacharprime}f\ gterm\ {\isacharequal}\ Apply\ {\isacharprime}f\ {\isachardoublequote}{\isacharprime}f\ gterm\ list{\isachardoublequote}\isanewline |
10469 | 10 |
\isanewline |
11866 | 11 |
\isamarkupfalse% |
11187 | 12 |
\isacommand{datatype}\ integer{\isacharunderscore}op\ {\isacharequal}\ Number\ int\ {\isacharbar}\ UnaryMinus\ {\isacharbar}\ Plus\isanewline |
10469 | 13 |
\isanewline |
11866 | 14 |
\isamarkupfalse% |
11187 | 15 |
\isacommand{consts}\ gterms\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}f\ set\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline |
11866 | 16 |
\isamarkupfalse% |
11187 | 17 |
\isacommand{inductive}\ {\isachardoublequote}gterms\ F{\isachardoublequote}\isanewline |
10469 | 18 |
\isakeyword{intros}\isanewline |
11187 | 19 |
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ \ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline |
20 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ gterms\ F{\isachardoublequote}\isanewline |
|
10469 | 21 |
\isanewline |
11866 | 22 |
\isamarkupfalse% |
11187 | 23 |
\isacommand{lemma}\ gterms{\isacharunderscore}mono{\isacharcolon}\ {\isachardoublequote}F{\isasymsubseteq}G\ {\isasymLongrightarrow}\ gterms\ F\ {\isasymsubseteq}\ gterms\ G{\isachardoublequote}\isanewline |
11866 | 24 |
\isamarkupfalse% |
15481 | 25 |
\isamarkupfalse% |
11866 | 26 |
\isamarkupfalse% |
27 |
\isamarkuptrue% |
|
28 |
\isamarkupfalse% |
|
15481 | 29 |
\isamarkupfalse% |
11866 | 30 |
% |
11187 | 31 |
\begin{isamarkuptext}% |
32 |
\begin{isabelle}% |
|
14470 | 33 |
\ \ \ \ \ {\isasymlbrakk}a\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ a\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}a\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharsemicolon}\ n\ {\isasymin}\ Even{\isachardot}even{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\isanewline |
34 |
\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ P% |
|
11173 | 35 |
\end{isabelle} |
36 |
\rulename{even.cases} |
|
10469 | 37 |
|
38 |
Just as a demo I include |
|
39 |
the two forms that Markus has made available. First the one for binding the |
|
40 |
result to a name% |
|
11187 | 41 |
\end{isamarkuptext}% |
11866 | 42 |
\isamarkuptrue% |
11187 | 43 |
\isacommand{inductive{\isacharunderscore}cases}\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\isanewline |
44 |
\ \ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequote}\isanewline |
|
10365 | 45 |
\isanewline |
11866 | 46 |
\isamarkupfalse% |
47 |
\isacommand{thm}\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases\isamarkupfalse% |
|
48 |
% |
|
11187 | 49 |
\begin{isamarkuptext}% |
50 |
\begin{isabelle}% |
|
14470 | 51 |
\ \ \ \ \ {\isasymlbrakk}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ n\ {\isasymin}\ Even{\isachardot}even\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P% |
11187 | 52 |
\end{isabelle} |
11173 | 53 |
\rulename{Suc_Suc_cases} |
10469 | 54 |
|
10457 | 55 |
and now the one for local usage:% |
11187 | 56 |
\end{isamarkuptext}% |
11866 | 57 |
\isamarkuptrue% |
11187 | 58 |
\isacommand{lemma}\ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline |
11866 | 59 |
\isamarkupfalse% |
60 |
\isamarkupfalse% |
|
15481 | 61 |
\isanewline |
11866 | 62 |
\isamarkupfalse% |
63 |
\isacommand{inductive{\isacharunderscore}cases}\ gterm{\isacharunderscore}Apply{\isacharunderscore}elim\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isachardoublequote}\isamarkupfalse% |
|
64 |
% |
|
11187 | 65 |
\begin{isamarkuptext}% |
10469 | 66 |
this is what we get: |
10457 | 67 |
|
11187 | 68 |
\begin{isabelle}% |
69 |
\ \ \ \ \ {\isasymlbrakk}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P% |
|
10469 | 70 |
\end{isabelle} |
11187 | 71 |
\rulename{gterm_Apply_elim}% |
72 |
\end{isamarkuptext}% |
|
11866 | 73 |
\isamarkuptrue% |
11187 | 74 |
\isacommand{lemma}\ gterms{\isacharunderscore}IntI\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\isanewline |
75 |
\ \ \ \ \ {\isachardoublequote}t\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}{\isachardoublequote}\isanewline |
|
11866 | 76 |
\isamarkupfalse% |
15481 | 77 |
\isamarkupfalse% |
11866 | 78 |
\isamarkuptrue% |
79 |
\isamarkupfalse% |
|
15481 | 80 |
\isamarkupfalse% |
11866 | 81 |
% |
11187 | 82 |
\begin{isamarkuptext}% |
83 |
\begin{isabelle}% |
|
84 |
\ \ \ \ \ mono\ f\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isasymsubseteq}\ f\ A\ {\isasyminter}\ f\ B% |
|
11173 | 85 |
\end{isabelle} |
11187 | 86 |
\rulename{mono_Int}% |
87 |
\end{isamarkuptext}% |
|
11866 | 88 |
\isamarkuptrue% |
11187 | 89 |
\isacommand{lemma}\ gterms{\isacharunderscore}Int{\isacharunderscore}eq\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline |
90 |
\ \ \ \ \ {\isachardoublequote}gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}\ {\isacharequal}\ gterms\ F\ {\isasyminter}\ gterms\ G{\isachardoublequote}\isanewline |
|
11866 | 91 |
\isamarkupfalse% |
15481 | 92 |
\isamarkupfalse% |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11866
diff
changeset
|
93 |
% |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11866
diff
changeset
|
94 |
\begin{isamarkuptext}% |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11866
diff
changeset
|
95 |
the following declaration isn't actually used% |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11866
diff
changeset
|
96 |
\end{isamarkuptext}% |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11866
diff
changeset
|
97 |
\isamarkuptrue% |
11187 | 98 |
\isacommand{consts}\ integer{\isacharunderscore}arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}integer{\isacharunderscore}op\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
11866 | 99 |
\isamarkupfalse% |
10469 | 100 |
\isacommand{primrec}\isanewline |
11708 | 101 |
{\isachardoublequote}integer{\isacharunderscore}arity\ {\isacharparenleft}Number\ n{\isacharparenright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline |
102 |
{\isachardoublequote}integer{\isacharunderscore}arity\ UnaryMinus\ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline |
|
103 |
{\isachardoublequote}integer{\isacharunderscore}arity\ Plus\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{2}}{\isachardoublequote}\isanewline |
|
10469 | 104 |
\isanewline |
11866 | 105 |
\isamarkupfalse% |
11187 | 106 |
\isacommand{consts}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline |
11866 | 107 |
\isamarkupfalse% |
11187 | 108 |
\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline |
10365 | 109 |
\isakeyword{intros}\isanewline |
11187 | 110 |
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharsemicolon}\ \ \isanewline |
111 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline |
|
112 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline |
|
10365 | 113 |
\isanewline |
114 |
\isanewline |
|
11866 | 115 |
\isamarkupfalse% |
11187 | 116 |
\isacommand{consts}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline |
11866 | 117 |
\isamarkupfalse% |
11187 | 118 |
\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline |
10365 | 119 |
\isakeyword{intros}\isanewline |
11187 | 120 |
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}args\ {\isasymin}\ lists\ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharparenright}{\isacharsemicolon}\ \ \isanewline |
121 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline |
|
122 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline |
|
123 |
\isakeyword{monos}\ lists{\isacharunderscore}mono\isanewline |
|
10469 | 124 |
\isanewline |
11866 | 125 |
\isamarkupfalse% |
11187 | 126 |
\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline |
11866 | 127 |
\isamarkupfalse% |
15481 | 128 |
\isamarkupfalse% |
11866 | 129 |
\isamarkuptrue% |
15481 | 130 |
\isamarkupfalse% |
11866 | 131 |
\isamarkuptrue% |
132 |
\isamarkupfalse% |
|
15481 | 133 |
\isanewline |
10878 | 134 |
\isanewline |
135 |
\isanewline |
|
11866 | 136 |
\isamarkupfalse% |
11187 | 137 |
\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline |
11866 | 138 |
\isamarkupfalse% |
15481 | 139 |
\isamarkupfalse% |
11866 | 140 |
\isamarkuptrue% |
15481 | 141 |
\isamarkupfalse% |
11866 | 142 |
\isamarkuptrue% |
143 |
\isamarkupfalse% |
|
15481 | 144 |
\isamarkupfalse% |
11866 | 145 |
% |
11187 | 146 |
\begin{isamarkuptext}% |
147 |
\begin{isabelle}% |
|
148 |
\ \ \ \ \ lists\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isacharequal}\ lists\ A\ {\isasyminter}\ lists\ B% |
|
149 |
\end{isabelle}% |
|
150 |
\end{isamarkuptext}% |
|
11866 | 151 |
\isamarkuptrue% |
10469 | 152 |
% |
11187 | 153 |
\begin{isamarkuptext}% |
10469 | 154 |
the rest isn't used: too complicated. OK for an exercise though.% |
11187 | 155 |
\end{isamarkuptext}% |
11866 | 156 |
\isamarkuptrue% |
11187 | 157 |
\isacommand{consts}\ integer{\isacharunderscore}signature\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}integer{\isacharunderscore}op\ {\isacharasterisk}\ {\isacharparenleft}unit\ list\ {\isacharasterisk}\ unit{\isacharparenright}{\isacharparenright}\ set{\isachardoublequote}\isanewline |
11866 | 158 |
\isamarkupfalse% |
11187 | 159 |
\isacommand{inductive}\ {\isachardoublequote}integer{\isacharunderscore}signature{\isachardoublequote}\isanewline |
10365 | 160 |
\isakeyword{intros}\isanewline |
11187 | 161 |
Number{\isacharcolon}\ \ \ \ \ {\isachardoublequote}{\isacharparenleft}Number\ n{\isacharcomma}\ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequote}\isanewline |
162 |
UnaryMinus{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}UnaryMinus{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequote}\isanewline |
|
163 |
Plus{\isacharcolon}\ \ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}Plus{\isacharcomma}\ \ \ \ \ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharparenright}{\isacharcomma}{\isacharparenleft}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequote}\isanewline |
|
10469 | 164 |
\isanewline |
165 |
\isanewline |
|
11866 | 166 |
\isamarkupfalse% |
11187 | 167 |
\isacommand{consts}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}f\ gterm\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}set{\isachardoublequote}\isanewline |
11866 | 168 |
\isamarkupfalse% |
11187 | 169 |
\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline |
10469 | 170 |
\isakeyword{intros}\isanewline |
11187 | 171 |
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline |
172 |
\ \ \ \ {\isachardoublequote}{\isasymlbrakk}{\isasymforall}pair\ {\isasymin}\ set\ args{\isachardot}\ pair\ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isacharsemicolon}\ \isanewline |
|
173 |
\ \ \ \ \ \ sig\ f\ {\isacharequal}\ {\isacharparenleft}map\ snd\ args{\isacharcomma}\ rtype{\isacharparenright}{\isasymrbrakk}\isanewline |
|
174 |
\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ {\isacharparenleft}map\ fst\ args{\isacharparenright}{\isacharcomma}\ rtype{\isacharparenright}\ \isanewline |
|
175 |
\ \ \ \ \ \ \ \ \ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline |
|
10469 | 176 |
\isanewline |
11866 | 177 |
\isamarkupfalse% |
11187 | 178 |
\isacommand{consts}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}f\ gterm\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}set{\isachardoublequote}\isanewline |
11866 | 179 |
\isamarkupfalse% |
11187 | 180 |
\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline |
10469 | 181 |
\isakeyword{intros}\isanewline |
11187 | 182 |
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline |
183 |
\ \ \ \ {\isachardoublequote}{\isasymlbrakk}args\ {\isasymin}\ lists{\isacharparenleft}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isacharparenright}{\isacharsemicolon}\ \isanewline |
|
184 |
\ \ \ \ \ \ sig\ f\ {\isacharequal}\ {\isacharparenleft}map\ snd\ args{\isacharcomma}\ rtype{\isacharparenright}{\isasymrbrakk}\isanewline |
|
185 |
\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ {\isacharparenleft}map\ fst\ args{\isacharparenright}{\isacharcomma}\ rtype{\isacharparenright}\ \isanewline |
|
186 |
\ \ \ \ \ \ \ \ \ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline |
|
187 |
\isakeyword{monos}\ lists{\isacharunderscore}mono\isanewline |
|
10365 | 188 |
\isanewline |
189 |
\isanewline |
|
11866 | 190 |
\isamarkupfalse% |
11187 | 191 |
\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline |
11866 | 192 |
\isamarkupfalse% |
193 |
\isamarkupfalse% |
|
194 |
\isamarkupfalse% |
|
195 |
\isamarkupfalse% |
|
15481 | 196 |
\isanewline |
11866 | 197 |
\isamarkupfalse% |
11187 | 198 |
\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline |
11866 | 199 |
\isamarkupfalse% |
200 |
\isamarkupfalse% |
|
201 |
\isamarkupfalse% |
|
202 |
\isamarkupfalse% |
|
15481 | 203 |
\isanewline |
10365 | 204 |
\isanewline |
11866 | 205 |
\isamarkupfalse% |
10365 | 206 |
\isacommand{end}\isanewline |
207 |
\isanewline |
|
11866 | 208 |
\isamarkupfalse% |
11187 | 209 |
\end{isabellebody}% |
10365 | 210 |
%%% Local Variables: |
211 |
%%% mode: latex |
|
212 |
%%% TeX-master: "root" |
|
213 |
%%% End: |