diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 34d5edd..fb551d3 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -231,12 +231,6 @@ $$(\exists A)\left[ \emptyset \in A \land (\forall a \in A) a^+ \in A\right].$$ - \begin{note} - Since the definition of natural numbers in Lean satisfies the properties - required by this axiom, there is no need to explicitly state the axiom - separately in Lean. - \end{note} - \lean{Prelude}{Nat} \lean{Mathlib/Init/Set}{Set.univ} diff --git a/preamble.tex b/preamble.tex index 7d59526..8eaf150 100644 --- a/preamble.tex +++ b/preamble.tex @@ -4,13 +4,13 @@ \usepackage[shortlabels]{enumitem} \usepackage{etoolbox} \usepackage{environ} -\usepackage{fancybox} \usepackage{fontawesome5} \usepackage{mathabx, mathrsfs} \usepackage{soul} \usepackage{stmaryrd} -% Must load `xcolor` before `tikz`. +% Must load `xcolor` before `tcolorbox` and `tikz`. \usepackage[dvipsnames]{xcolor} +\usepackage{tcolorbox} \usepackage{tikz} % `hyperref` comes after `xr-hyper`. \usepackage{xr-hyper} @@ -91,18 +91,18 @@ % Admonitions % ======================================== -\newcommand{\@admonition}[2]{% - \begin{center} - \doublebox{ - \begin{minipage}{0.95\textwidth} - \vspace{2pt} - \hl{#1} #2 - \vspace{2pt} - \end{minipage}} - \end{center}} - -\NewEnviron{note}{\@admonition{NOTE:}{\BODY}} -\NewEnviron{todo}{\@admonition{TODO:}{\BODY}} +\NewEnviron{note}{% + \begin{tcolorbox}[% + sharp corners, + fonttitle=\sffamily\bfseries, + toptitle=2pt, + bottomtitle=2pt, + coltitle=black!80!white, + colback=yellow!30, + colframe=yellow!80!black, + title=Note] + \BODY + \end{tcolorbox}} % ======================================== % Statements