equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 % |
|
2 \begin{isabellebody}% |
2 % |
3 % |
3 \begin{isamarkuptext}% |
4 \begin{isamarkuptext}% |
4 \noindent |
5 \noindent |
5 The task is to develop a compiler from a generic type of expressions (built |
6 The task is to develop a compiler from a generic type of expressions (built |
6 up from variables, constants and binary operations) to a stack machine. This |
7 up from variables, constants and binary operations) to a stack machine. This |
109 We could now go back and prove \isa{exec (comp e) s [] = [value e s]} |
110 We could now go back and prove \isa{exec (comp e) s [] = [value e s]} |
110 merely by simplification with the generalized version we just proved. |
111 merely by simplification with the generalized version we just proved. |
111 However, this is unnecessary because the generalized version fully subsumes |
112 However, this is unnecessary because the generalized version fully subsumes |
112 its instance.% |
113 its instance.% |
113 \end{isamarkuptext}% |
114 \end{isamarkuptext}% |
114 \end{isabelle}% |
115 \end{isabellebody}% |
115 %%% Local Variables: |
116 %%% Local Variables: |
116 %%% mode: latex |
117 %%% mode: latex |
117 %%% TeX-master: "root" |
118 %%% TeX-master: "root" |
118 %%% End: |
119 %%% End: |