diff options
| author | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-04-30 12:26:13 +0200 |
|---|---|---|
| committer | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-04-30 12:26:13 +0200 |
| commit | cfd5061ced34f061e84ecca2a266f8f4cd01ce36 (patch) | |
| tree | 2298a5c7ab0f64e97abbdc0ab2d9635720de30c8 /latex/naproche.sty | |
| parent | 6eea98cf3e66a07251e6370ea948898799d5055b (diff) | |
Adding the first formalisation of reals
Diffstat (limited to 'latex/naproche.sty')
| -rw-r--r-- | latex/naproche.sty | 5 |
1 files changed, 3 insertions, 2 deletions
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 |