# HG changeset patch
# User paulson
# Date 1117009940 -7200
# Node ID d8a6afbb71ecb6d4dad081dba0fa1ddd01e824a5
# Parent  e0136cdef722e18702e26187a6819a56eeea904a
new environments for Proof General notes

diff -r e0136cdef722 -r d8a6afbb71ec doc-src/TutorialI/pgchest.pdf
Binary file doc-src/TutorialI/pgchest.pdf has changed
diff -r e0136cdef722 -r d8a6afbb71ec doc-src/TutorialI/pghead.pdf
Binary file doc-src/TutorialI/pghead.pdf has changed
diff -r e0136cdef722 -r d8a6afbb71ec doc-src/TutorialI/tutorial.sty
--- a/doc-src/TutorialI/tutorial.sty	Wed May 25 10:18:09 2005 +0200
+++ b/doc-src/TutorialI/tutorial.sty	Wed May 25 10:32:20 2005 +0200
@@ -109,14 +109,29 @@
 \def\_{\leavevmode\kern.06em\vbox{\hrule height.2ex width.3em}\hskip0.1em}
 
 
-%%%% ``WARNING'' environment
-\def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}}
+%%%% ``WARNING'' environment: 2 ! characters separated by negative thin space
+\def\warnbang{\vtop to 0pt{\vss\hbox{\Huge\bf!\!!}\vss}}
 \newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 
          \small %%WAS\baselineskip=0.9\baselineskip
          \noindent \hangindent\parindent \hangafter=-2 
-         \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
+         \hbox to0pt{\hskip-\hangindent\warnbang\hfill}\ignorespaces}%
         {\par\endgroup\medbreak}
 
+%%%% ``PROOF GENERAL'' environment: full chest
+\def\pgchest{\lower3pt\vbox to 0pt{\vss\hbox{\includegraphics[width=12pt]{pgchest}}\vss}}
+\newenvironment{pgnote}{\medskip\medbreak\begingroup \clubpenalty=10000 
+         \small \noindent \hangindent\parindent \hangafter=-2 
+         \hbox to0pt{\hskip-\hangindent \pgchest\hfill}\ignorespaces}%
+  {\par\endgroup\medbreak}
+
+%%%% ``PROOF GENERAL'' environment: head only
+\def\pghead{\lower3pt\vbox to 0pt{\vss\hbox{\includegraphics[width=12pt]{pghead}}\vss}}
+\newenvironment{pgnoteh}{\medskip\medbreak\begingroup \clubpenalty=10000 
+         \small \noindent \hangindent\parindent \hangafter=-2 
+         \hbox to0pt{\hskip-\hangindent \pghead\hfill}\ignorespaces}%
+  {\par\endgroup\medbreak}
+
+
 
 %%%% Standard logical symbols
 \let\turn=\vdash