From cfd5061ced34f061e84ecca2a266f8f4cd01ce36 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 30 Apr 2024 12:26:13 +0200 Subject: Adding the first formalisation of reals --- latex/naproche.sty | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'latex/naproche.sty') diff --git a/latex/naproche.sty b/latex/naproche.sty index d975f21..cb65fe7 100644 --- a/latex/naproche.sty +++ b/latex/naproche.sty @@ -127,8 +127,9 @@ \newcommand{\Univ}[1]{\fun{Univ}(#1)} \newcommand{\upward}[2]{#2^{\uparrow #1}} \newcommand{\LeftOrb}[2]{#2\cdot #1} -\newcommand{\addpair}{\mathcal{H}} -%\newcommand{\add}[2]{(#1 + #2)} +\newcommand{\integers}{\mathcal{Z}} +\newcommand{\zero}{0} +\newcommand{\one}{1} \newcommand\restrl[2]{{% we make the whole thing an ordinary symbol -- cgit v1.2.3