isabelle: lib/texinputs/isabelle.sty@05688a1a4f41 (annotated)

7709 545637744a85 macros for Isabelle generated LaTeX output; wenzelm parents: diff changeset	1	%%
545637744a85 macros for Isabelle generated LaTeX output; wenzelm parents: diff changeset	2	%% $Id$
545637744a85 macros for Isabelle generated LaTeX output; wenzelm parents: diff changeset	3	%%
545637744a85 macros for Isabelle generated LaTeX output; wenzelm parents: diff changeset	4	%% macros for Isabelle generated LaTeX output
545637744a85 macros for Isabelle generated LaTeX output; wenzelm parents: diff changeset	5	%%
545637744a85 macros for Isabelle generated LaTeX output; wenzelm parents: diff changeset	6
545637744a85 macros for Isabelle generated LaTeX output; wenzelm parents: diff changeset	7	%%% Simple document preparation (based on theory token language)
545637744a85 macros for Isabelle generated LaTeX output; wenzelm parents: diff changeset	8
8713 05688a1a4f41 global \isa@parindent, \isa@parskip; wenzelm parents: 8662 diff changeset	9	% basic isabelle environment
7788 825b8b1ad136 removed verbatim markups; wenzelm parents: 7771 diff changeset	10
8713 05688a1a4f41 global \isa@parindent, \isa@parskip; wenzelm parents: 8662 diff changeset	11	\newcommand{\isabelledefaultstyle}{\small\tt\slshape}
8474 ae32be343647 renamed isabelle env; wenzelm parents: 8232 diff changeset	12	\newcommand{\isabellestyle}{}
8713 05688a1a4f41 global \isa@parindent, \isa@parskip; wenzelm parents: 8662 diff changeset	13
05688a1a4f41 global \isa@parindent, \isa@parskip; wenzelm parents: 8662 diff changeset	14	\newdimen\isa@parindent\newdimen\isa@parskip
8474 ae32be343647 renamed isabelle env; wenzelm parents: 8232 diff changeset	15	\newenvironment{isabelle}{%
8713 05688a1a4f41 global \isa@parindent, \isa@parskip; wenzelm parents: 8662 diff changeset	16	\isa@parindent\parindent\parindent0pt%
05688a1a4f41 global \isa@parindent, \isa@parskip; wenzelm parents: 8662 diff changeset	17	\isa@parskip\parskip\parskip0pt%
05688a1a4f41 global \isa@parindent, \isa@parskip; wenzelm parents: 8662 diff changeset	18	\isabelledefaultstyle\isabellestyle}{}
05688a1a4f41 global \isa@parindent, \isa@parskip; wenzelm parents: 8662 diff changeset	19
05688a1a4f41 global \isa@parindent, \isa@parskip; wenzelm parents: 8662 diff changeset	20	\newcommand{\isa}[1]{\emph{\isabelledefaultstyle\isabellestyle #1}}
05688a1a4f41 global \isa@parindent, \isa@parskip; wenzelm parents: 8662 diff changeset	21
7709 545637744a85 macros for Isabelle generated LaTeX output; wenzelm parents: diff changeset	22	\newcommand{\isanewline}{\mbox{}\\\mbox{}}
7752 7ee322caf59c accomodate markup commands; wenzelm parents: 7709 diff changeset	23
7797 38a46d9ea08a improved special chars; wenzelm parents: 7788 diff changeset	24	\chardef\isabraceleft=`\{
38a46d9ea08a improved special chars; wenzelm parents: 7788 diff changeset	25	\chardef\isabraceright=`\}
38a46d9ea08a improved special chars; wenzelm parents: 7788 diff changeset	26	\chardef\isatilde=`\~
38a46d9ea08a improved special chars; wenzelm parents: 7788 diff changeset	27	\chardef\isacircum=`\^
38a46d9ea08a improved special chars; wenzelm parents: 7788 diff changeset	28	\chardef\isabackslash=`\\
7788 825b8b1ad136 removed verbatim markups; wenzelm parents: 7771 diff changeset	29
7797 38a46d9ea08a improved special chars; wenzelm parents: 7788 diff changeset	30
38a46d9ea08a improved special chars; wenzelm parents: 7788 diff changeset	31	% keyword and section markup
7788 825b8b1ad136 removed verbatim markups; wenzelm parents: 7771 diff changeset	32
7918 2979b3b75dbd achieve proper italic correction; wenzelm parents: 7907 diff changeset	33	\newcommand{\isacommand}[1]{\emph{\bf #1}}
2979b3b75dbd achieve proper italic correction; wenzelm parents: 7907 diff changeset	34	\newcommand{\isakeyword}[1]{\emph{\bf #1}}
7797 38a46d9ea08a improved special chars; wenzelm parents: 7788 diff changeset	35	\newcommand{\isabeginblock}{\isakeyword{\{}}
38a46d9ea08a improved special chars; wenzelm parents: 7788 diff changeset	36	\newcommand{\isaendblock}{\isakeyword{\}}}
7758 d36c19045493 tuned markup commands; wenzelm parents: 7752 diff changeset	37
8501 2ff3d25943f1 \isamarkupheader: \section; wenzelm parents: 8489 diff changeset	38	\newcommand{\isamarkupheader}[1]{\section{#1}}
7752 7ee322caf59c accomodate markup commands; wenzelm parents: 7709 diff changeset	39	\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
7ee322caf59c accomodate markup commands; wenzelm parents: 7709 diff changeset	40	\newcommand{\isamarkupsection}[1]{\section{#1}}
7ee322caf59c accomodate markup commands; wenzelm parents: 7709 diff changeset	41	\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
7ee322caf59c accomodate markup commands; wenzelm parents: 7709 diff changeset	42	\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
7ee322caf59c accomodate markup commands; wenzelm parents: 7709 diff changeset	43	\newcommand{\isamarkupsect}[1]{\section{#1}}
7ee322caf59c accomodate markup commands; wenzelm parents: 7709 diff changeset	44	\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
7ee322caf59c accomodate markup commands; wenzelm parents: 7709 diff changeset	45	\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
8662 f9679ddbc492 isapar, isamarkuptext, isamarkuptxt turned into environments; wenzelm parents: 8512 diff changeset	46
8713 05688a1a4f41 global \isa@parindent, \isa@parskip; wenzelm parents: 8662 diff changeset	47	\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\par\medskip}{\par\smallskip}
8662 f9679ddbc492 isapar, isamarkuptext, isamarkuptxt turned into environments; wenzelm parents: 8512 diff changeset	48	\newenvironment{isamarkuptext}{\normalsize\rm\begin{isapar}}{\end{isapar}}
f9679ddbc492 isapar, isamarkuptext, isamarkuptxt turned into environments; wenzelm parents: 8512 diff changeset	49	\newenvironment{isamarkuptxt}{\rm\begin{isapar}}{\end{isapar}}
7758 d36c19045493 tuned markup commands; wenzelm parents: 7752 diff changeset	50	\newcommand{\isamarkupcmt}[1]{{\rm--- #1}}

author	wenzelm
	Fri, 14 Apr 2000 15:55:40 +0200
changeset 8713	05688a1a4f41
parent 8662	f9679ddbc492
child 8714	61cafd91963c
permissions	-rw-r--r--