\relax 
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{2}}
\citation{nocuts}
\citation{nfu}
\@writefile{toc}{\contentsline {section}{\numberline {2}The Language: Parsing, Display, Declarations}{4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Tokens}{4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Syntax}{7}}
\@writefile{toc}{\contentsline {section}{\numberline {3}Set Theory and Defined Notions}{9}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}The Stratification Algorithm}{11}}
\@writefile{toc}{\contentsline {section}{\numberline {4}Proof Trees and The Logic of Propositions}{12}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1}Sequents}{12}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2}Proof Trees}{14}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.3}Sequent Rules in General}{16}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.4}Specific Sequent Rules: Connectives}{16}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.5}Axiom}{17}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.6}Left rules}{17}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.7}Right rules}{17}}
\@writefile{toc}{\contentsline {section}{\numberline {5}Variables and Substitution}{18}}
\@writefile{toc}{\contentsline {section}{\numberline {6}More Sequent Rules}{19}}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.1}Rules for Quantifiers}{19}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.1.1}Left Rules}{19}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.1.2}Right Rules}{20}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.1.3}Comments on Quantifier Rules}{20}}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.2}Rules for Membership}{20}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.2.1}Left Rule}{20}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.2.2}Right Rule}{20}}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.3}Rules for Equality}{21}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.1}Left Rule}{21}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.2}Right Rule}{21}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.3}Comments on Equality Rules}{21}}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.4}Global Substitution, manual and automatic}{21}}
\@writefile{toc}{\contentsline {section}{\numberline {7}Proving and Using Theorems}{22}}
\@writefile{toc}{\contentsline {section}{\numberline {8}Cut and ``Theorem Cut''}{22}}
\@writefile{toc}{\contentsline {section}{\numberline {9}The Theorem List and Reading Saved Proofs}{23}}
\@writefile{toc}{\contentsline {section}{\numberline {10}Alternative Logics}{23}}
\@writefile{toc}{\contentsline {section}{\numberline {11}Future Developments}{24}}
\@writefile{toc}{\contentsline {section}{\numberline {12}Examples of Use of Marcel}{24}}
\@writefile{toc}{\contentsline {section}{\numberline {13}Command Reference}{36}}
\@writefile{toc}{\contentsline {subsection}{\numberline {13.1}Commands Listed Alphabetically}{36}}
\@writefile{toc}{\contentsline {subsection}{\numberline {13.2}Commands in Categories by Function}{44}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {13.2.1}Prover Settings}{44}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {13.2.2}Declaring Primitives and Syntax}{44}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {13.2.3}Axioms, Definitions, and Theorems}{46}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {13.2.4}Proof Manipulations}{47}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {13.2.5}Starting and Finishing Sequents}{48}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {13.2.6}Sequent Manipulations}{49}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {13.2.7}Lists and Displays}{51}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {13.2.8}History}{52}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {13.2.9}Loading and Saving}{53}}