doc-src/proof209.sty
 author oheimb Sat Feb 15 16:10:00 1997 +0100 (1997-02-15) changeset 2628 1fe7c9f599c2 parent 1210 230b9b4b783e permissions -rw-r--r--
description of del(eq)congs, safe and unsafe solver
 paulson@1210  1 % proof.sty (Proof Figure Macros)  paulson@1210  2 %  paulson@1210  3 % version 2.0  paulson@1210  4 % June 24, 1991  paulson@1210  5 % Copyright (C) 1990,1991 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)  paulson@1210  6 %  paulson@1210  7 % This program is free software; you can redistribute it or modify  paulson@1210  8 % it under the terms of the GNU General Public License as published by  paulson@1210  9 % the Free Software Foundation; either versions 1, or (at your option)  paulson@1210  10 % any later version.  paulson@1210  11 %  paulson@1210  12 % This program is distributed in the hope that it will be useful  paulson@1210  13 % but WITHOUT ANY WARRANTY; without even the implied warranty of  paulson@1210  14 % MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the  paulson@1210  15 % GNU General Public License for more details.  paulson@1210  16 %  paulson@1210  17 % Usage:  paulson@1210  18 % In \documentstyle, specify an optional style proof', say,  paulson@1210  19 % \documentstyle[proof]{article}.  paulson@1210  20 %  paulson@1210  21 % The following macros are available:  paulson@1210  22 %  paulson@1210  23 % In all the following macros, all the arguments such as  paulson@1210  24 % and are processed in math mode.  paulson@1210  25 %  paulson@1210  26 % \infer  paulson@1210  27 % draws an inference.  paulson@1210  28 %  paulson@1210  29 % Use & in to delimit upper formulae.  paulson@1210  30 % consists more than 0 formulae.  paulson@1210  31 %  paulson@1210  32 % \infer returns \hbox{ ... } or \vbox{ ... } and  paulson@1210  33 % sets \@LeftOffset and \@RightOffset globally.  paulson@1210  34 %  paulson@1210  35 % \infer[