%%
%% This is file `natded.sty',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%
%% natded.dtx  (with options: `package')
%% 
%% This is a generated file.
%% 
%% Copyright (c) 2006 Tikitu de Jager <tikitu@gmail.com>
%% 
%% This file may be distributed and/or modified under the conditions of
%% the LaTeX Project Public License, either version 1.2 of this license
%% or (at your option) any later version.  The latest version of this
%% license is in:
%% 
%%    http://www.latex-project.org/lppl.txt
%% 
%% and version 1.2 or later is part of all distributions of LaTeX version
%% 1999/12/01 or later.
%% 
\NeedsTeXFormat{LaTeX2e}[1999/12/01]
\ProvidesPackage{natded}[06/09/25 v0.2 Natural deduction proofs]
%\RequirePackage{}
\newtoks\ass@toks
\newcounter{assumpties}
\newcounter{afleidingregel}
\newcounter{afleidingen}
\setcounter{afleidingen}{0}
\newcommand{\ass@space}{\hspace{5pt}}
\newcommand{\ass@ul@hook}{\vrule height 3pt\hspace{-0.4pt}%
  \vrule width 0.5em height 3pt depth -2.6pt\hspace{-0.4pt}}
\newcommand{\ass@dr@hook}{\vrule depth -8pt\hspace{-0.4pt}%
  \vrule width 0.5em height 7.9pt depth -7.5pt\hspace{-0.4pt}}
\newcommand{\ass@u@fill}{\leaders\hbox{\vrule height 3pt
                                              depth -2.6pt}\hfill\hbox{}}
\newcommand{\ass@d@fill}{\leaders\hbox{\vrule height 7.9pt
                                              depth -7.5pt}\hfill\hbox{}}
\newcommand{\ass@push}{%
  \edef\tmp{\the\ass@toks}%
  \global\ass@toks=\expandafter{\expandafter\vline\expandafter\ass@space\tmp}}
\def\ass@pop@sub#1\ass@space#2\e@ass@pop{\global\ass@toks={#2}}
\newcommand{\ass@pop}{\expandafter\ass@pop@sub\the\ass@toks\e@ass@pop}
\newcommand{\ass@print}{\unskip\the\ass@toks}
\newcommand{\proof@line@label}[1]{%
  \def\tempa{}\def\tempb{#1}%
  \ifx\tempa\tempb%
  \else\expandafter\label\expandafter{\roman{afleidingen}:line:#1}\fi}
\newcommand{\proof@line@ref}[1]{\expandafter\ref{\roman{afleidingen}:line:#1}}
\newcommand{\print@proof@line}{\arabic{afleidingregel}.}
\newcommand{\proof@line@refs}[2]{%
  \def\tempa{}\def\tempb{#2}\ifx\tempa\tempb\else{#1}\fi%
  \line@refs #2,\e@line@refs}
\def\gobble@line@refs#1\e@line@refs{}
\def\line@refs#1,#2\e@line@refs{%
  \let\next@line@refs=\gobble@line@refs%
  \def\tempa{#1}\def\tempb{}\ifx\tempa\tempb\else%
    \proof@line@ref{#1}%
    \def\tempa{#2}\ifx\tempa\tempb\let\next@line@refs=\gobble@line@refs\else%
      \let\next@line@refs=\line@refs,
    \fi
  \fi
  \next@line@refs#2\e@line@refs%
}
\newcommand{\proof@rule}[3]{\unskip\ass@print
  &\refstepcounter{afleidingregel}\print@proof@line\proof@line@label{#1}
  &\ensuremath{#2} &#3\\\ignorespaces}
\newcommand{\anonregel}[3][1]{\unskip\proof@rule{#1}{#2}{#3}}
\def\premis{%
  \unskip\@ifnextchar[{\premis@i}{\premis@i[] }%]
}
\def\premis@i[#1] $#2${%
  \unskip\proof@rule{#1}{#2}{prem.}%
}
\def\regel{%
  \unskip\@ifnextchar[{\regel@i}{\regel@i[] }%]
}
\def\regel@i[#1] $#2$ #3 {%
  \unskip\@ifnextchar({\regel@ii[#1] #3 $#2$ }{\regel@ii[#1] #3 $#2$ ()}%)
}
\def\regel@ii[#1] #2 $#3$ (#4){%
  \unskip\proof@rule{#1}{#3}{$\csname #2\endcsname$\proof@line@refs{: }{#4}}%
}
\newenvironment{assumptie}{%
  \unskip\@ifnextchar[{\assumptie@sub}{\assumptie@sub[] }%]
}{\unskip%
  \addtocounter{assumpties}{-1}%
  \ifnum\value{assumpties}<0%
  \errhelp{You seem to have retracted an assumption you haven't made. LaTeX
    would normally warn you that your environments don't match, but this is
    more helpful, don't you think?}%
  \errmessage{Retraction of an unmade assumption}%
  \fi
  \ass@pop
  \unskip\ass@print\ass@dr@hook\ass@d@fill
  &\hspace{-.5em}\ass@d@fill
  &\hspace{-.5em}\ass@d@fill\\[-.8em]%
  \begingroup\def\@currenvir{assumptie}\ignorespaces}

\def\assumptie@sub[#1] $#2${%
  \unskip%
  \stepcounter{assumpties}%
  \endgroup%
  \ass@print\ass@ul@hook\ass@u@fill
  &\refstepcounter{afleidingregel}\print@proof@line\proof@line@label{#1}
  &\ensuremath{#2} &assumption\ass@push\\\ignorespaces}
\newenvironment{afleiding}{%
  \setcounter{assumpties}{0}%
  \setcounter{afleidingregel}{0}%
  \stepcounter{afleidingen}%
  \ass@toks={}%
  \begin{tabular}{l@{\hspace{0.4em}}l@{\hspace{0.4em}}ll}%
}{
  \ifnum\value{assumpties}>0
  \errhelp{Some assumption(s) in the afleiding have not been retracted
    before the end of the proof. This means your afleiding is broken!}
  \errmessage{Assumptions still active at end of afleiding}
  \fi
  \end{tabular}
}
\newcommand{\intro@regel}[1]{\textrm{I}_{#1}}
\newcommand{\elim@regel}[1]{\textrm{E}_{#1}}
\newcommand{\mk@intro@regel}[2]{%
  \expandafter\newcommand\csname I#1\endcsname{\intro@regel{#2}}}
\newcommand{\mk@elim@regel}[2]{%
  \expandafter\newcommand\csname E#1\endcsname{\elim@regel{#2}}}
\DeclareOption{prop}{
  \mk@intro@regel{conj}{\land}
  \mk@elim@regel{conj}{\land}
  \mk@intro@regel{disj}{\lor}
  \mk@elim@regel{disj}{\lor}
  \mk@intro@regel{neg}{\lnot}
  \mk@elim@regel{neg}{\lnot}
  \mk@elim@regel{pijl}{\rightarrow}
  \mk@intro@regel{pijl}{\rightarrow}
  \newcommand{\EFSQ}{\textrm{EFSQ}}
  \newcommand{\negneg}{\ensuremath{\lnot\lnot}}
  \newcommand{\herhaling}{\textrm{her.}}
}
\DeclareOption{pred}{
  \mk@intro@regel{univ}{\forall}
  \mk@elim@regel{univ}{\forall}
  \mk@intro@regel{exist}{\exists}
  \mk@elim@regel{exist}{\exists}
}
\DeclareOption{intuit}{
  \renewcommand{\negneg}{
    \errhelp{The double-negation rule is not allowed in intuitionistic
      derivations. If you meant to write a classical derivation, don't use
      the package option [intuit].}
    \errmessage{Double-negation rule in intuitionistic afleiding}
  }
}
\ProcessOptions\relax
\InputIfFileExists{natded.cfg}{}{}
\endinput
%%
%% End of file `natded.sty'.