From e7c38a5516246b751b89535594075f6f95a243fd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 4 Oct 2015 22:17:46 +0200 Subject: RefMan, ch. 4: In chapter 4 about CIC, renounced to keep a local context for discharge in global declarations. Discharge now done on a global declaration. Hence removed Def and Assum which were only partially used (e.g. in rules Def and Assum but not in delta-conversion, nor in rule Const). Added discharge rule over definitions using let-in. It replaces the "substitution" rule since about 7.0. --- 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 573c3c812..f785a85bb 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -412,6 +412,7 @@ \newcommand{\Fix}[2]{\mbox{\tt Fix}~#1\{#2\}} \newcommand{\CoFix}[2]{\mbox{\tt CoFix}~#1\{#2\}} \newcommand{\With}[2]{\mbox{\tt ~with~}} +\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\substs}[4]{#1\{(#2/#3)_{#4}\}} \newcommand{\Sort}{\mbox{$\cal S$}} -- cgit v1.2.3