doc-src/TutorialI/CodeGen/document/CodeGen.tex
changeset 9145 9f7b8de5bfaf
parent 8771 026f37a86ea7
child 9458 c613cd06d5cf
equal deleted inserted replaced
9144:20a70ef9c320 9145:9f7b8de5bfaf
   110 merely by simplification with the generalized version we just proved.
   110 merely by simplification with the generalized version we just proved.
   111 However, this is unnecessary because the generalized version fully subsumes
   111 However, this is unnecessary because the generalized version fully subsumes
   112 its instance.%
   112 its instance.%
   113 \end{isamarkuptext}%
   113 \end{isamarkuptext}%
   114 \end{isabelle}%
   114 \end{isabelle}%
       
   115 %%% Local Variables:
       
   116 %%% mode: latex
       
   117 %%% TeX-master: "root"
       
   118 %%% End: