Isabelle/Isar macros;
authorwenzelm
Fri Jul 30 15:57:27 1999 +0200 (1999-07-30)
changeset 71380a17c2a93454
parent 7137 e5d18fd42430
child 7139 1af4c1f48368
Isabelle/Isar macros;
doc-src/isar.sty
     1.1 --- a/doc-src/isar.sty	Fri Jul 30 15:56:58 1999 +0200
     1.2 +++ b/doc-src/isar.sty	Fri Jul 30 15:57:27 1999 +0200
     1.3 @@ -1,63 +1,75 @@
     1.4  
     1.5  %% $Id$
     1.6 +%%
     1.7 +%% Isar language elements
     1.8 +%%
     1.9  
    1.10  \usepackage{ifthen}
    1.11  
    1.12 -%Isar language elements
    1.13 -\newcommand{\I@keyword}[1]{{\mathord{\mathbf{#1}}}}
    1.14 +\newcommand{\isarkeyword}[1]{{\mathord{\mathbf{#1}}}}
    1.15 +
    1.16 +\newcommand{\indexisarcmd}[1]{\index{#1 (command)|bold}}
    1.17 +\newcommand{\isarcmd}[1]{\isarkeyword{#1}}
    1.18 +\newcommand{\isartrans}[2]{#1 \mathbin{\,\to\,} #2}
    1.19 +\newcommand{\isarkeep}[1]{#1 \mathbin{\,\to\,} #1}
    1.20 +
    1.21  \newcommand{\I@optname}[1]{\ifthenelse{\equal{}{#1}}{}{~#1\colon}}
    1.22  \newcommand{\I@optoptname}[1]{\ifthenelse{\equal{}{#1}}{}{~[#1\colon]}}
    1.23  \newcommand{\I@optmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~(#1)}}
    1.24  \newcommand{\I@optoptmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~[(#1)]}}
    1.25  
    1.26 -\newcommand{\LEMMANAME}{\I@keyword{lemma}}
    1.27 -\newcommand{\THEOREMNAME}{\I@keyword{theorem}}
    1.28 -\newcommand{\NOTENAME}{\I@keyword{note}}
    1.29 -\newcommand{\FROMNAME}{\I@keyword{from}}
    1.30 -\newcommand{\WITHNAME}{\I@keyword{with}}
    1.31 -\newcommand{\FIXNAME}{\I@keyword{fix}}
    1.32 -\newcommand{\ASSUMENAME}{\I@keyword{assume}}
    1.33 -\newcommand{\PRESUMENAME}{\I@keyword{presume}}
    1.34 -\newcommand{\HAVENAME}{\I@keyword{have}}
    1.35 -\newcommand{\SHOWNAME}{\I@keyword{show}}
    1.36 -\newcommand{\HENCENAME}{\I@keyword{hence}}
    1.37 -\newcommand{\THUSNAME}{\I@keyword{thus}}
    1.38 -\newcommand{\PROOFNAME}{\I@keyword{proof}}
    1.39 -\newcommand{\QEDNAME}{\I@keyword{qed}}
    1.40 -\newcommand{\BYNAME}{\I@keyword{by}}
    1.41 -\newcommand{\ISNAME}{\I@keyword{is}}
    1.42 -\newcommand{\CONCLNAME}{\I@keyword{concl}}
    1.43 -\newcommand{\LETNAME}{\I@keyword{let}}
    1.44 -\newcommand{\DEFNAME}{\I@keyword{def}}
    1.45 -\newcommand{\SUFFNAME}{\I@keyword{suffient}}
    1.46 -\newcommand{\CMTNAME}{\I@keyword{-{}-}}
    1.47 +\newcommand{\LEMMANAME}{\isarkeyword{lemma}}
    1.48 +\newcommand{\THEOREMNAME}{\isarkeyword{theorem}}
    1.49 +\newcommand{\NOTENAME}{\isarkeyword{note}}
    1.50 +\newcommand{\FROMNAME}{\isarkeyword{from}}
    1.51 +\newcommand{\WITHNAME}{\isarkeyword{with}}
    1.52 +\newcommand{\FIXNAME}{\isarkeyword{fix}}
    1.53 +\newcommand{\ASSUMENAME}{\isarkeyword{assume}}
    1.54 +\newcommand{\PRESUMENAME}{\isarkeyword{presume}}
    1.55 +\newcommand{\HAVENAME}{\isarkeyword{have}}
    1.56 +\newcommand{\SHOWNAME}{\isarkeyword{show}}
    1.57 +\newcommand{\HENCENAME}{\isarkeyword{hence}}
    1.58 +\newcommand{\THUSNAME}{\isarkeyword{thus}}
    1.59 +\newcommand{\PROOFNAME}{\isarkeyword{proof}}
    1.60 +\newcommand{\QEDNAME}{\isarkeyword{qed}}
    1.61 +\newcommand{\BYNAME}{\isarkeyword{by}}
    1.62 +\newcommand{\ISNAME}{\isarkeyword{is}}
    1.63 +\newcommand{\CONCLNAME}{\isarkeyword{concl}}
    1.64 +\newcommand{\LETNAME}{\isarkeyword{let}}
    1.65 +\newcommand{\DEFNAME}{\isarkeyword{def}}
    1.66 +\newcommand{\SUFFNAME}{\isarkeyword{suffient}}
    1.67 +\newcommand{\CMTNAME}{\isarkeyword{-{}-}}
    1.68  
    1.69 -\newcommand{\TYPES}{\I@keyword{types}}
    1.70 -\newcommand{\CONSTS}{\I@keyword{consts}}
    1.71 -\newcommand{\DEFS}{\I@keyword{defs}}
    1.72 +\newcommand{\THEORY}{\isarkeyword{theory}}
    1.73 +\newcommand{\CONTEXT}{\isarkeyword{context}}
    1.74 +\newcommand{\END}{\isarkeyword{end}}
    1.75 +
    1.76 +\newcommand{\TYPES}{\isarkeyword{types}}
    1.77 +\newcommand{\CONSTS}{\isarkeyword{consts}}
    1.78 +\newcommand{\DEFS}{\isarkeyword{defs}}
    1.79 +\newcommand{\TEXT}{\isarkeyword{text}}
    1.80 +\newcommand{\TXT}{\isarkeyword{txt}}
    1.81  \newcommand{\NOTE}[2]{\NOTENAME~#1=#2}
    1.82  \newcommand{\FROM}[1]{\FROMNAME~#1}
    1.83  \newcommand{\WITH}[1]{\WITHNAME~#1}
    1.84  \newcommand{\FIX}[1]{\FIXNAME~#1}
    1.85  \newcommand{\ASSUME}[2]{\ASSUMENAME\I@optname{#1}~#2}
    1.86  \newcommand{\PRESUME}[2]{\PRESUMENAME\I@optname{#1}~#2}
    1.87 -\newcommand{\THEN}{\I@keyword{then}}
    1.88 -\newcommand{\BEGIN}{\I@keyword{begin}}
    1.89 -\newcommand{\END}{\I@keyword{end}}
    1.90 -\newcommand{\BG}{\lceil}
    1.91 -\newcommand{\EN}{\rfloor}
    1.92 -\newcommand{\HAVE}[2]{\I@keyword{have}\I@optname{#1}~#2}
    1.93 -\newcommand{\SHOW}[2]{\I@keyword{show}\I@optname{#1}~#2}
    1.94 -\newcommand{\HENCE}[2]{\I@keyword{hence}\I@optname{#1}~#2}
    1.95 -\newcommand{\THUS}[2]{\I@keyword{thus}\I@optname{#1}~#2}
    1.96 +\newcommand{\THEN}{\isarkeyword{then}}
    1.97 +\newcommand{\BG}{\{\{}
    1.98 +\newcommand{\EN}{\}\}}
    1.99 +\newcommand{\HAVE}[2]{\isarkeyword{have}\I@optname{#1}~#2}
   1.100 +\newcommand{\SHOW}[2]{\isarkeyword{show}\I@optname{#1}~#2}
   1.101 +\newcommand{\HENCE}[2]{\isarkeyword{hence}\I@optname{#1}~#2}
   1.102 +\newcommand{\THUS}[2]{\isarkeyword{thus}\I@optname{#1}~#2}
   1.103  \newcommand{\LEMMA}[2]{\LEMMANAME\I@optname{#1}~#2}
   1.104  \newcommand{\THEOREM}[2]{\THEOREMNAME\I@optname{#1}~#2}
   1.105  \newcommand{\PROOF}[1]{\PROOFNAME\I@optmeth{#1}}
   1.106  \newcommand{\PPROOF}[1]{\PPROOFNAME\I@optmeth{#1}}
   1.107  \newcommand{\QED}[1]{\QEDNAME\I@optmeth{#1}}
   1.108  \newcommand{\BY}[1]{\BYNAME\I@optmeth{#1}}
   1.109 -\newcommand{\DOT}{\I@keyword{.}}
   1.110 -\newcommand{\DDOT}{\I@keyword{.\,.}}
   1.111 +\newcommand{\DOT}{\isarkeyword{.}}
   1.112 +\newcommand{\DDOT}{\isarkeyword{.\,.}}
   1.113  \newcommand{\DDDOT}{\dots}
   1.114  \newcommand{\IS}[1]{(\ISNAME~#1)}
   1.115  \newcommand{\LET}[1]{\LETNAME~#1}
   1.116 @@ -66,5 +78,5 @@
   1.117  \newcommand{\SUFF}[1]{\SUFFNAME~#1}
   1.118  \newcommand{\ATT}[1]{\ap [#1]}
   1.119  \newcommand{\CMT}[1]{\CMTNAME~\text{#1}}
   1.120 -\newcommand{\ALSO}{\I@keyword{also}}
   1.121 -\newcommand{\FINALLY}{\I@keyword{finally}}
   1.122 +\newcommand{\ALSO}{\isarkeyword{also}}
   1.123 +\newcommand{\FINALLY}{\isarkeyword{finally}}