Hets - the Heterogeneous Tool Set
Copyright(c) Klaus Luettich C. Maeder Uni Bremen 2005
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerluecke@informatik.uni-bremen.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

Common.ProofUtils

Description

Functions useful for all prover connections in Hets

Some were moved from Isabelle.Translate and some others from Isabelle.IsaProve.

Synopsis

Documentation

prepareSenNames :: (String -> String) -> [Named a] -> [Named a] Source #

translate special characters in sentence names

disambiguateSens :: Set String -> [Named a] -> [Named a] Source #

disambiguate sentence names

genericDisambigSens :: Int -> (a -> String) -> (String -> a -> a) -> Set String -> [a] -> [a] Source #

generically disambiguate lists with names

nameSens :: [Named a] -> [Named a] Source #

name unlabeled axioms with Axnnn

collectNameMapping :: [Named a] -> [Named a] -> Map String String Source #

collect the mapping of new to old names

lookupCharMap :: Char -> String Source #

charMap :: Map Char String Source #

a separate Map speeds up lookup