equal
deleted
inserted
replaced
138 & & \isa{FOL} \\ |
138 & & \isa{FOL} \\ |
139 & $\swarrow$ & & $\searrow$ & \\ |
139 & $\swarrow$ & & $\searrow$ & \\ |
140 \isa{Nat} & & & & \isa{List} \\ |
140 \isa{Nat} & & & & \isa{List} \\ |
141 & $\searrow$ & & $\swarrow$ \\ |
141 & $\searrow$ & & $\swarrow$ \\ |
142 & & \isa{Length} \\ |
142 & & \isa{Length} \\ |
143 & & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\ |
143 & & \multicolumn{3}{l}{~~\mbox{\isa{\isakeyword{imports}}}} \\ |
144 & & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\ |
144 & & \multicolumn{3}{l}{~~\mbox{\isa{\isakeyword{begin}}}} \\ |
145 & & $\vdots$~~ \\ |
145 & & $\vdots$~~ \\ |
146 & & \isa{{\isasymbullet}}~~ \\ |
146 & & \isa{{\isasymbullet}}~~ \\ |
147 & & $\vdots$~~ \\ |
147 & & $\vdots$~~ \\ |
148 & & \isa{{\isasymbullet}}~~ \\ |
148 & & \isa{{\isasymbullet}}~~ \\ |
149 & & $\vdots$~~ \\ |
149 & & $\vdots$~~ \\ |
150 & & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\ |
150 & & \multicolumn{3}{l}{~~\mbox{\isa{\isacommand{end}}}} \\ |
151 \end{tabular} |
151 \end{tabular} |
152 \caption{A theory definition depending on ancestors}\label{fig:ex-theory} |
152 \caption{A theory definition depending on ancestors}\label{fig:ex-theory} |
153 \end{center} |
153 \end{center} |
154 \end{figure} |
154 \end{figure} |
155 |
155 |