diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-09 15:57:52 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:06 +0100 |
| commit | 8654b03544f0efe4b418a0afdc871ff84784ff83 (patch) | |
| tree | 6c223fdaaa28fa6710fcd16ba64af3e5d6087638 /doc/common | |
| parent | 6beb39ff5e8e52692cc008e4b43ee28ecf792f8a (diff) | |
RefMan, ch. 4: Adding discharging of inductive types.
Diffstat (limited to 'doc/common')
| -rw-r--r-- | doc/common/macros.tex | 1 |
1 files changed, 1 insertions, 0 deletions
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}} |