# HG changeset patch
# User haftmann
# Date 1285336437 -7200
# Node ID e75b993c04334598330b7f460c77669820cf29ab
# Parent  6814630157b9afa87aa046e602825f25e2107434# Parent  2ef15ec8e7dc4ea856a30c01f3c025d25dbce89b
merged

diff -r 6814630157b9 -r e75b993c0433 doc-src/Codegen/Thy/Evaluation.thy
--- a/doc-src/Codegen/Thy/Evaluation.thy	Fri Sep 24 15:14:55 2010 +0200
+++ b/doc-src/Codegen/Thy/Evaluation.thy	Fri Sep 24 15:53:57 2010 +0200
@@ -162,25 +162,27 @@
 
 subsection {* Schematic overview *}
 
-(*FIXME rotatebox?*)
-
 text {*
+  \newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont}
+  \fontsize{9pt}{12pt}\selectfont
   \begin{tabular}{ll||c|c|c}
     & & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
-    dynamic & interactive evaluation 
+    \multirow{5}{1ex}{\rotatebox{90}{dynamic}}
+      & interactive evaluation 
       & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"}
       \tabularnewline
-    & plain evaluation & & & @{ML "Code_Evaluation.dynamic_value"} \tabularnewline \hline
+    & plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5}
     & evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
-    & property conversion & & & @{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \hline
-    & conversion & @{ML "Code_Simp.dynamic_eval_conv"} & @{ML "Nbe.dynamic_eval_conv"}
-      & @{ML "Code_Evaluation.dynamic_eval_conv"} \tabularnewline \hline \hline
-    static & plain evaluation & & & @{ML "Code_Evaluation.static_value"} \tabularnewline \hline
+    & property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5}
+    & conversion & \ttsize@{ML "Code_Simp.dynamic_eval_conv"} & \ttsize@{ML "Nbe.dynamic_eval_conv"}
+      & \ttsize@{ML "Code_Evaluation.dynamic_eval_conv"} \tabularnewline \hline \hline
+    \multirow{3}{1ex}{\rotatebox{90}{static}}
+      & plain evaluation & & & \ttsize@{ML "Code_Evaluation.static_value"} \tabularnewline \cline{2-5}
     & property conversion & &
-      & @{ML "Code_Runtime.static_holds_conv"} \tabularnewline \hline
-    & conversion & @{ML "Code_Simp.static_eval_conv"}
-      & @{ML "Nbe.static_eval_conv"}
-      & @{ML "Code_Evaluation.static_eval_conv"}
+      & \ttsize@{ML "Code_Runtime.static_holds_conv"} \tabularnewline \cline{2-5}
+    & conversion & \ttsize@{ML "Code_Simp.static_eval_conv"}
+      & \ttsize@{ML "Nbe.static_eval_conv"}
+      & \ttsize@{ML "Code_Evaluation.static_eval_conv"}
   \end{tabular}
 *}
 
diff -r 6814630157b9 -r e75b993c0433 doc-src/Codegen/Thy/document/Evaluation.tex
--- a/doc-src/Codegen/Thy/document/Evaluation.tex	Fri Sep 24 15:14:55 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex	Fri Sep 24 15:53:57 2010 +0200
@@ -217,22 +217,26 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-\begin{tabular}{ll||c|c|c}
+\newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont}
+  \fontsize{9pt}{12pt}\selectfont
+  \begin{tabular}{ll||c|c|c}
     & & \isa{simp} & \isa{nbe} & \isa{code} \tabularnewline \hline \hline
-    dynamic & interactive evaluation 
+    \multirow{5}{1ex}{\rotatebox{90}{dynamic}}
+      & interactive evaluation 
       & \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isacharbrackleft}simp{\isacharbrackright}} & \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isacharbrackleft}nbe{\isacharbrackright}} & \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isacharbrackleft}code{\isacharbrackright}}
       \tabularnewline
-    & plain evaluation & & & \verb|Code_Evaluation.dynamic_value| \tabularnewline \hline
+    & plain evaluation & & & \ttsize\verb|Code_Evaluation.dynamic_value| \tabularnewline \cline{2-5}
     & evaluation method & \hyperlink{method.code-simp}{\mbox{\isa{code{\isacharunderscore}simp}}} & \hyperlink{method.normalization}{\mbox{\isa{normalization}}} & \hyperlink{method.eval}{\mbox{\isa{eval}}} \tabularnewline
-    & property conversion & & & \verb|Code_Runtime.dynamic_holds_conv| \tabularnewline \hline
-    & conversion & \verb|Code_Simp.dynamic_eval_conv| & \verb|Nbe.dynamic_eval_conv|
-      & \verb|Code_Evaluation.dynamic_eval_conv| \tabularnewline \hline \hline
-    static & plain evaluation & & & \verb|Code_Evaluation.static_value| \tabularnewline \hline
+    & property conversion & & & \ttsize\verb|Code_Runtime.dynamic_holds_conv| \tabularnewline \cline{2-5}
+    & conversion & \ttsize\verb|Code_Simp.dynamic_eval_conv| & \ttsize\verb|Nbe.dynamic_eval_conv|
+      & \ttsize\verb|Code_Evaluation.dynamic_eval_conv| \tabularnewline \hline \hline
+    \multirow{3}{1ex}{\rotatebox{90}{static}}
+      & plain evaluation & & & \ttsize\verb|Code_Evaluation.static_value| \tabularnewline \cline{2-5}
     & property conversion & &
-      & \verb|Code_Runtime.static_holds_conv| \tabularnewline \hline
-    & conversion & \verb|Code_Simp.static_eval_conv|
-      & \verb|Nbe.static_eval_conv|
-      & \verb|Code_Evaluation.static_eval_conv|
+      & \ttsize\verb|Code_Runtime.static_holds_conv| \tabularnewline \cline{2-5}
+    & conversion & \ttsize\verb|Code_Simp.static_eval_conv|
+      & \ttsize\verb|Nbe.static_eval_conv|
+      & \ttsize\verb|Code_Evaluation.static_eval_conv|
   \end{tabular}%
 \end{isamarkuptext}%
 \isamarkuptrue%
diff -r 6814630157b9 -r e75b993c0433 doc-src/Codegen/codegen.tex
--- a/doc-src/Codegen/codegen.tex	Fri Sep 24 15:14:55 2010 +0200
+++ b/doc-src/Codegen/codegen.tex	Fri Sep 24 15:53:57 2010 +0200
@@ -2,6 +2,7 @@
 \documentclass[12pt,a4paper,fleqn]{article}
 \usepackage{latexsym,graphicx}
 \usepackage[refpage]{nomencl}
+\usepackage{multirow}
 \usepackage{../iman,../extra,../isar,../proof}
 \usepackage{../isabelle,../isabellesym}
 \usepackage{style}