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