# HG changeset patch # User wenzelm # Date 939226466 -7200 # Node ID d36c19045493efcd62c20b7cc39e5fdd9acc3e7e # Parent b2538dccc21ef5faa4083509ca0ee82418408383 tuned markup commands; diff -r b2538dccc21e -r d36c19045493 lib/texinputs/isabelle.sty --- a/lib/texinputs/isabelle.sty Wed Oct 06 18:12:48 1999 +0200 +++ b/lib/texinputs/isabelle.sty Wed Oct 06 18:14:26 1999 +0200 @@ -14,16 +14,20 @@ \newcommand{\isacommand}[1]{{\bf #1}} \newcommand{\isakeyword}[1]{{\bf #1}} -%theory sections -\newcommand{\isamarkupheader}[1]{{\rm #1}} + +%section markup + +\newcommand{\isapar}[1]{{\par\medskip #1\par\smallskip}} + +\newcommand{\isamarkupheader}[1]{\isapar{\normalsize\rm #1}} \newcommand{\isamarkupchapter}[1]{\chapter{#1}} \newcommand{\isamarkupsection}[1]{\section{#1}} \newcommand{\isamarkupsubsection}[1]{\subsection{#1}} \newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}} -\newcommand{\isamarkuptext}[1]{{\rm #1}} +\newcommand{\isamarkuptext}[1]{\isapar{\normalsize\rm #1}} -%proof sections \newcommand{\isamarkupsect}[1]{\section{#1}} \newcommand{\isamarkupsubsect}[1]{\subsection{#1}} \newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}} -\newcommand{\isamarkuptxt}[1]{{\sl #1}} +\newcommand{\isamarkuptxt}[1]{\isapar{\rm #1}} +\newcommand{\isamarkupcmt}[1]{{\rm--- #1}}