equal
deleted
inserted
replaced
1 % pr(latex xsymbols symbols) |
1 % pr(latex xsymbols symbols) |
2 \documentclass[11pt,a4paper]{report} |
2 \documentclass{article} |
3 \newif\ifremarks |
3 \newif\ifremarks |
4 \remarkstrue %TRUE causes remarks to be displayed (as marginal notes) |
4 \remarkstrue %TRUE causes remarks to be displayed (as marginal notes) |
5 \usepackage{isabelle,isabellesym} |
5 \usepackage{cl2emono-modified,isabelle,isabellesym} |
6 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment} |
6 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment} |
7 \usepackage{proof,amsmath} |
7 \usepackage{proof,amsmath} |
8 \usepackage{../pdfsetup} %last package! |
8 \usepackage{../pdfsetup} %last package! |
9 |
9 |
10 %\newtheorem{theorem}{Theorem}[section] |
10 %\newtheorem{theorem}{Theorem}[section] |
24 \newcommand{\isasymuniqex}{\isamath{\exists!\,}} |
24 \newcommand{\isasymuniqex}{\isamath{\exists!\,}} |
25 |
25 |
26 \renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}} |
26 \renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}} |
27 |
27 |
28 %% lcp's macros |
28 %% lcp's macros |
29 \newcommand{\remark}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi} |
29 \newcommand{\REMARK}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi} |
30 \newcommand{\rulename}[1]{\hfill$(\text{#1})$} %names of Isabelle rules |
30 \newcommand{\rulename}[1]{\hfill$(\text{#1})$} %names of Isabelle rules |
31 \let\bigisa=\isa |
31 \let\bigisa=\isa |
32 %% was previously |
32 %% was previously |
33 %% \newcommand{\bigisa}[1]{\texttt{\textsl{#1}}} |
33 %% \newcommand{\bigisa}[1]{\texttt{\textsl{#1}}} |
34 %% because \isa is too small for variables, but does it really matter? |
34 %% because \isa is too small for variables, but does it really matter? |