doc-src/IsarAdvanced/Functions/functions.tex
changeset 29750 3197b895f858
parent 26911 871cc7f11034
equal deleted inserted replaced
29749:5a576282c935 29750:3197b895f858
     1 
       
     2 %% $Id$
       
     3 
     1 
     4 \documentclass[a4paper,fleqn]{article}
     2 \documentclass[a4paper,fleqn]{article}
     5 
     3 
     6 \usepackage{latexsym,graphicx}
     4 \usepackage{latexsym,graphicx}
     7 \usepackage[refpage]{nomencl}
     5 \usepackage[refpage]{nomencl}
    17 \newcommand{\isasymINFIX}{\cmd{infix}}
    15 \newcommand{\isasymINFIX}{\cmd{infix}}
    18 \newcommand{\isasymLOCALE}{\cmd{locale}}
    16 \newcommand{\isasymLOCALE}{\cmd{locale}}
    19 \newcommand{\isasymINCLUDES}{\cmd{includes}}
    17 \newcommand{\isasymINCLUDES}{\cmd{includes}}
    20 \newcommand{\isasymDATATYPE}{\cmd{datatype}}
    18 \newcommand{\isasymDATATYPE}{\cmd{datatype}}
    21 \newcommand{\isasymAXCLASS}{\cmd{axclass}}
    19 \newcommand{\isasymAXCLASS}{\cmd{axclass}}
    22 \newcommand{\isasymFIXES}{\cmd{fixes}}
       
    23 \newcommand{\isasymASSUMES}{\cmd{assumes}}
       
    24 \newcommand{\isasymDEFINES}{\cmd{defines}}
    20 \newcommand{\isasymDEFINES}{\cmd{defines}}
    25 \newcommand{\isasymNOTES}{\cmd{notes}}
    21 \newcommand{\isasymNOTES}{\cmd{notes}}
    26 \newcommand{\isasymSHOWS}{\cmd{shows}}
       
    27 \newcommand{\isasymCLASS}{\cmd{class}}
    22 \newcommand{\isasymCLASS}{\cmd{class}}
    28 \newcommand{\isasymINSTANCE}{\cmd{instance}}
    23 \newcommand{\isasymINSTANCE}{\cmd{instance}}
    29 \newcommand{\isasymLEMMA}{\cmd{lemma}}
    24 \newcommand{\isasymLEMMA}{\cmd{lemma}}
    30 \newcommand{\isasymPROOF}{\cmd{proof}}
    25 \newcommand{\isasymPROOF}{\cmd{proof}}
    31 \newcommand{\isasymQED}{\cmd{qed}}
    26 \newcommand{\isasymQED}{\cmd{qed}}