factored out TSTP/SPASS/Vampire proof parsing;
from "Sledgehammer_Reconstructo" to a new module "ATP_Proof"
(* Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
*)
header {* The Hoare logic for Bali. *}
theory Bali
imports AxExample AxSound AxCompl Trans
begin
end