equal
deleted
inserted
replaced
212 have "$\neg$ zeroable (STAR r)" "[] $\in$ L (r) ^ 0" by simp_all |
212 have "$\neg$ zeroable (STAR r)" "[] $\in$ L (r) ^ 0" by simp_all |
213 then show "zeroable (STAR r) $\longleftrightarrow$ (L (STAR r) = {})" |
213 then show "zeroable (STAR r) $\longleftrightarrow$ (L (STAR r) = {})" |
214 by (simp (no_asm) add: Star_def) blast |
214 by (simp (no_asm) add: Star_def) blast |
215 qed |
215 qed |
216 \end{lstlisting} |
216 \end{lstlisting} |
217 \caption{An Isabelle proof about the function \pcode{zeroable}.\label{proof}} |
217 \caption{An Isabelle proof about the function \texttt{zeroable}.\label{proof}} |
218 \end{figure} |
218 \end{figure} |
219 |
219 |
220 \end{document} |
220 \end{document} |
221 |
221 |
222 %%% Local Variables: |
222 %%% Local Variables: |