Email Gateway (Aug 19 2022 at 09:52): Email Gateway (Aug 19 2022 at 09:52):From: John Wickerson <jpw48@cam.ac.uk>
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
Last updated: Apr 19 2024 at 20:15 UTC