# Other articles

Thunderlink is a fantastically useful add-on for the Thunderbird mail user agent. It lets you create links to email that you can put into all sorts of documents (like ToDo lists or notes). The links use the URI scheme thunderlink that needs to be handled by whatever mechanism you use …

2. # Make Firefox play embedded MP4 videos

Date: 2015-01-03

Tags: tools

For some reason (at least on Mac OS X and according to a quick search also on other platforms) Firefox does not play MP4 videos embedded into websites using the <video> tag. Seems that enabling the two config options media.fragmented-mp4.enabled and media.fragmented-mp4.exposed fixes the issue.

3. # vim-like ctrl+v enter in Emacs

Date: 2012-12-17 (updated: 2022-09-21)

Tags: tools

Suppose you have a list like this

foo, bar, baz, quux


in your Emacs buffer, but you’d rather have one element per line like this

foo
bar
baz
quux


What to do? In vim this is easy:

:%s/,/^M/g


where ^M is inserted using

Ctrl+v


But what …

4. # Thunderbird line breaking behaviour

Because I keep forgetting which options to set to force Thunderbird to send and display line breaks instead of flowed plain text emails that may or may not come out right at the other end (usually those emails exhibit unsightly long lines which among other things might make quoting from …

5. # Snippets for LaTeX + Emacs users

I've been using Emacs to edit LaTeX for some time now, mostly resorting to AUCTeX#s keyboard commands to insert fonts, environments and some other stuff that I need in some documents. But I'm also a big fan of yasnippet, the de facto standard for inserting more or less complex …

6. # Several ways to prove a simple proposition

Date: 2011-02-17

Tags: coq

Coq provides many tactics. In this post we show a number of proofs that use different tactics to prove a simple proposition of first order logic, namely $$\forall P\;Q,\, P \wedge Q \rightarrow Q \wedge P$$ which in Coq translates to

forall P Q : Prop, P /\ Q -> Q /\ P …
7. # Using Qucs for filter design

Qucs, short for Quite Universal Circuit Simulator, is as the name suggests a simulation package for electronic circuits. It's free and sports a nice graphical schematic capture interface. One of its many nice and useful features is the ability to write equations so you can calculate all kinds of stuff …

8. # Beginning Ltac

Date: 2011-02-10

Tags: coq

One of the strong points of Coq is its powerful proof automation facility embodied in the tactic language $$\mathcal{L}_{tac}$$. Instead of having to write new tactics in ML, compiling them, and jumping through all sorts of hoops in the process, we can simply write down new tactics …

9. # How to draw commutative diagrams in LaTeX with TikZ

Date: 2011-02-02 (updated: 2022-10-02)

Sooner or later everyone who uses LaTeX to typeset documents containing maths will encounter the problem of how to draw commutative diagrams. There are many packages, some general purpose other specialized for the task. An excellent survey of some of these alternatives by James Milne can be found here.

I …

10. # Another script font for LaTeX

Sometimes it’s nice to have an extra script font available to make distinctions between different kinds of objects clearer. One such font is Ralph Smith’s Formal Script (see here for the TeX Catalogue entry) which is provided by the mathrsfs package.

This gives you a new LaTeX font …