doc-src/Intro/intro.toc
changeset 1085 504dad4d7843
parent 359 b5a2e9503a7a
equal deleted inserted replaced
1084:502a61cbf37b 1085:504dad4d7843
    49 \contentsline {subsection}{\numberline {10.1}Deriving a rule using tactics and meta-level assumptions}{39}
    49 \contentsline {subsection}{\numberline {10.1}Deriving a rule using tactics and meta-level assumptions}{39}
    50 \contentsline {subsection}{\numberline {10.2}Definitions and derived rules}{41}
    50 \contentsline {subsection}{\numberline {10.2}Definitions and derived rules}{41}
    51 \contentsline {subsection}{\numberline {10.3}Deriving the $\neg $ introduction rule}{41}
    51 \contentsline {subsection}{\numberline {10.3}Deriving the $\neg $ introduction rule}{41}
    52 \contentsline {subsection}{\numberline {10.4}Deriving the $\neg $ elimination rule}{42}
    52 \contentsline {subsection}{\numberline {10.4}Deriving the $\neg $ elimination rule}{42}
    53 \contentsline {section}{\numberline {11}Defining theories}{44}
    53 \contentsline {section}{\numberline {11}Defining theories}{44}
    54 \contentsline {subsection}{\numberline {11.1}Declaring constants and rules}{46}
    54 \contentsline {subsection}{\numberline {11.1}Declaring constants, definitions and rules}{46}
    55 \contentsline {subsection}{\numberline {11.2}Declaring type constructors}{46}
    55 \contentsline {subsection}{\numberline {11.2}Declaring type constructors}{46}
    56 \contentsline {subsection}{\numberline {11.3}Type synonyms}{48}
    56 \contentsline {subsection}{\numberline {11.3}Type synonyms}{48}
    57 \contentsline {subsection}{\numberline {11.4}Infix and mixfix operators}{48}
    57 \contentsline {subsection}{\numberline {11.4}Infix and mixfix operators}{48}
    58 \contentsline {subsection}{\numberline {11.5}Overloading}{50}
    58 \contentsline {subsection}{\numberline {11.5}Overloading}{50}
    59 \contentsline {section}{\numberline {12}Theory example: the natural numbers}{51}
    59 \contentsline {section}{\numberline {12}Theory example: the natural numbers}{51}