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 Source #

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

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

printNamedSen :: Named Sentence -> Doc Source #

printing a named sentence

printTerm :: Term -> Doc Source #

print plain term

Orphan instances

Pretty ProofMethod Source # 
Instance details

Methods

pretty :: ProofMethod -> Doc Source #

pretties :: [ProofMethod] -> Doc Source #

Pretty Modifier Source # 
Instance details

Methods

pretty :: Modifier -> Doc Source #

pretties :: [Modifier] -> Doc Source #

Pretty ProofEnd Source # 
Instance details

Methods

pretty :: ProofEnd -> Doc Source #

pretties :: [ProofEnd] -> Doc Source #

Pretty ProofCommand Source # 
Instance details

Methods

pretty :: ProofCommand -> Doc Source #

pretties :: [ProofCommand] -> Doc Source #

Pretty IsaProof Source # 
Instance details

Methods

pretty :: IsaProof -> Doc Source #

pretties :: [IsaProof] -> Doc Source #

Pretty Sign Source # 
Instance details

Methods

pretty :: Sign -> Doc Source #

pretties :: [Sign] -> Doc Source #

Pretty Sentence Source # 
Instance details

Methods

pretty :: Sentence -> Doc Source #

pretties :: [Sentence] -> Doc Source #