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