From 8654b03544f0efe4b418a0afdc871ff84784ff83 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 9 Oct 2015 15:57:52 +0200
Subject: RefMan, ch. 4: Adding discharging of inductive types.

---
 doc/common/macros.tex | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc/common')

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index f785a85bb..88770affb 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -363,6 +363,7 @@
 \newcommand{\myifthenelse}[3]{\kw{if} ~ #1 ~\kw{then} ~ #2 ~ \kw{else} ~ #3}
 \newcommand{\fun}[2]{\item[]{\tt {#1}}. \quad\\ #2}
 \newcommand{\WF}[2]{\ensuremath{{\cal W\!F}(#1)[#2]}}
+\newcommand{\WFTWOLINES}[2]{\ensuremath{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}}
 \newcommand{\WFE}[1]{\WF{E}{#1}}
 \newcommand{\WT}[4]{\ensuremath{#1[#2] \vdash #3 : #4}}
 \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}
-- 
cgit v1.2.3