(* print natural deduction proof in tree format, headers.
   Copyright (C) 2003 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

open "natded_h";

extern val pfc_print_tree : 'a outstream * string *
	   (string gclause -> unit) * (string gclause -> unit) -> pfc list -> unit;
(* pfc_print_tree (f, prompt, pdef, pass) pfcl
 prints the proofs in pfcl on file f.
 Each proof starts with prompt.
 pdef and pass are used to print "by definition" and "by assumption" respectively.
 *)

