]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - macros.tex
Proved another lemma (aux1 + aux2)
[fireball-separation.git] / macros.tex
index 4c82f0b94616e233afb851958dfe90963813adec..4c30e1512cda8f659a4ff7d3a1c5a6677d6ba808 100644 (file)
@@ -1,10 +1,15 @@
+\usepackage{blindtext}\r
+\usepackage{enumerate}\r
+\usepackage{hyperref, bookmark}\r
+\usepackage{amsmath, amsfonts, amssymb, amsthm}\r
+\usepackage{xcolor}\r
 \usepackage{bussproofs}\r
 \r
 \theoremstyle{plain}\r
 \newtheorem{theorem}{Theorem}\r
 \newtheorem{lemma}{Lemma}\r
 % \newtheorem{prop}[thm]{Proposition}\r
-% \newtheorem*{cor}{Corollary}\r
+\newtheorem{corollary}{Corollary}\r
 \r
 \theoremstyle{definition}\r
 \newtheorem{definition}{Definition}\r
 \newcommand{\Numeral}[1]{\bar{#1}}\r
 \r
 \newcommand{\ToFire}[1]{#1{\downarrow}}\r
+\r
+\r
+% from strong_fireballs macros.tex\r
+\newcommand{\Lam}[1]{\lambda #1.\,}\r
+\r
+\newcommand{\hl}[1]{{\underline{#1}}}\r
+\newcommand{\Esub}[2]{\texttt{[}#2\texttt{/}#1\texttt{]}}\r
+\newcommand{\Comma}{\texttt{,}}\r
+\newcommand{\Semi}{\texttt{;}}\r
+\newcommand{\Subst}[2]{\{#2/#1\}}\r
+% \newcommand{\Comma}{}\r
+\newcommand{\tm}{t}\r
+\newcommand{\tmtwo}{u}\r
+\newcommand{\tmthree}{s}\r
+\newcommand{\var}{x}\r
+\newcommand{\vartwo}{y}\r
+\newcommand{\varthree}{z}\r
+\newcommand{\varfour}{w}\r
+\r
+\newcommand{\Red}[2]{\xrightarrow{#2}_{#1}}\r
+\newcommand{\TODO}{{\color{red}\textbf{TODO}}}\r
+\r
+\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}\r
+\renewcommand{\vec}{\overrightarrow}\r
+\newcommand{\reflemma}[1]{Lemma~\ref{l:#1}}\r
+\newcommand{\head}{h}\r
+\newcommand{\args}{a}\r