Hets - the Heterogeneous Tool Set

Copyright(c) University of Cambridge, Cambridge, England adaption (c) Till Mossakowski, Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

Isabelle.IsaPrint

Description

Printing functions for Isabelle logic.

Synopsis

Documentation

showBaseSig :: BaseSig -> String

printIsaTheory :: String -> Sign -> [Named Sentence] -> Doc

getAxioms :: [Named Sentence] -> ([Named Sentence], [Named Sentence])

printNamedSen :: Named Sentence -> Doc

printing a named sentence

printTerm :: Term -> Doc

print plain term