summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Wed, 26 Jan 2005 17:34:42 +0100 | |

changeset 15471 | e7f069887ec2 |

parent 15470 | 7e12ad2f6672 |

child 15472 | 4674102737e9 |

*** empty log message ***

doc-src/LaTeXsugar/IsaMakefile | file | annotate | diff | comparison | revisions | |

doc-src/LaTeXsugar/Sugar/Sugar.thy | file | annotate | diff | comparison | revisions |

--- a/doc-src/LaTeXsugar/IsaMakefile Wed Jan 26 16:39:44 2005 +0100 +++ b/doc-src/LaTeXsugar/IsaMakefile Wed Jan 26 17:34:42 2005 +0100 @@ -21,8 +21,9 @@ Sugar: $(LOG)/HOL-Sugar.gz -$(LOG)/HOL-Sugar.gz: Sugar/ROOT.ML Sugar/document/root.tex Sugar/document/root.bib \ - ../../HOL/Library/LaTeXsugar.thy ../../HOL/Library/OptinalSugar.thy +$(LOG)/HOL-Sugar.gz: Sugar/ROOT.ML Sugar/Sugar.thy \ + Sugar/document/root.tex Sugar/document/root.bib \ + ../../HOL/Library/LaTeXsugar.thy ../../HOL/Library/OptionalSugar.thy @$(USEDIR) HOL Sugar

--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Wed Jan 26 16:39:44 2005 +0100 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Wed Jan 26 17:34:42 2005 +0100 @@ -31,13 +31,17 @@ This document shows you how to make Isabelle and \LaTeX\ cooperate to produce ordinary looking mathematics that hides the fact that it was -typeset by a machine. You merely need to import theory -\texttt{LaTeXsugar} in the header of your own theory and copy the bits -of \texttt{OptionalSugar} that you want to use. You may also need -additional \LaTeX\ packages. These should be included at the beginning -of your \LaTeX\ document, typically in \texttt{root.tex}. +typeset by a machine. You merely need to load the right files: +\begin{itemize} +\item Import theory \texttt{LaTeXsugar} in the header of your own +theory. You may also want bits of \texttt{OptionalSugar}, which you can +copy selectively into your own theory or import as a whole. Both +theories live in \texttt{HOL/Library} and are found automatically. -The theories and support files are available from \cite{tar}. +\item Should you need additional \LaTeX\ packages (the text will tell +you so), you include them at the beginning of your \LaTeX\ document, +typically in \texttt{root.tex}. +\end{itemize} *} section{* HOL syntax*} @@ -139,7 +143,10 @@ G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"} \end{center} -Limitations: premises and conclusion must each not be longer than the line. +Limitations: 1. Premises and conclusion must each not be longer than +the line. 2. Premises that are @{text"\<Longrightarrow>"}-implications are again +displayed with a horizontal line, which looks at least unusual. + *} subsection{*If-then*} @@ -148,11 +155,11 @@ the body of \newtheorem{theorem}{Theorem} \begin{theorem} -@{thm[mode=IfThen,eta_contract=false] setsum_cartesian_product[no_vars]} +@{thm[mode=IfThen] zle_trans[no_vars]} \end{theorem} by typing \begin{quote} -\verb!@!\verb!{thm[mode=IfThen] setsum_cartesian_product[no_vars]}! +\verb!@!\verb!{thm[mode=IfThen] le_trans[no_vars]}! \end{quote} In order to prevent odd line breaks, the premises are put into boxes.