# [isabelle] isabelle logo as qed symbol

Dear all,

In a recent research paper, I formalised some of my theorems in Isabelle, but left some of them as just proved by hand. I thought it might be nice to use a different QED symbol depending on which method I had used, so I made a little symbol, based loosely on the Isabelle cubes logo.

In case anybody else would like to do something similar, here is some LaTeX/TikZ code for generating the symbol I used. There is a bit more info, and a picture, on the following page: http://johnwickerson.wordpress.com/2013/01/09/isabelle-qed/

\usepackage{tikz}
\newcommand{\isabelleqed}{%
\begin{tikzpicture}[x=0.8mm, y=0.8mm, baseline=-0.3mm, line join=round]
\begin{scope}[yslant=-0.5]
\draw (0,0) rectangle +(1,1);
\draw (2,1) rectangle +(1,1);
\draw (1,2) rectangle +(1,1);
\end{scope}
\begin{scope}[yslant=0.5]
\filldraw (1,-1) rectangle +(1,1);
\filldraw (3,-2) rectangle +(1,1);
\filldraw (2,0) rectangle +(1,1);
\end{scope}
\begin{scope}[yslant=0.5,xslant=-1]
\draw (1,0) rectangle +(1,1);
\draw (2,-1) rectangle +(1,1);
\draw (3,1) rectangle +(1,1);
\end{scope}
\end{tikzpicture}%
}

Best wishes,
John

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.