Hets - the Heterogeneous Tool Set

Copyright(c) C. Maeder and Uni Bremen 2005-2006
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

Isabelle.IsaParse

Description

parse the outer syntax of an Isabelle theory file. The syntax is taken from http://isabelle.in.tum.de/dist/Isabelle/doc/isar-ref.pdf for Isabelle2005 and is adjusted for Isabelle2011-1.

Synopsis

Documentation

parseTheory :: Parser (TheoryHead, Body) Source #

parses a complete isabelle theory file, but skips i.e. proofs

data Body Source #

The axioms, goals, constants and data types of a theory

Constructors

Body 

Fields

Instances

Show Body Source # 

Methods

showsPrec :: Int -> Body -> ShowS

show :: Body -> String

showList :: [Body] -> ShowS

data TheoryHead Source #

the theory part before and including the begin keyword with a context

Constructors

TheoryHead 

Fields

Instances

Eq TheoryHead Source # 

Methods

(==) :: TheoryHead -> TheoryHead -> Bool

(/=) :: TheoryHead -> TheoryHead -> Bool

data SimpValue a Source #

Constructors

SimpValue 

Fields

Instances

Eq a => Eq (SimpValue a) Source # 

Methods

(==) :: SimpValue a -> SimpValue a -> Bool

(/=) :: SimpValue a -> SimpValue a -> Bool

Show a => Show (SimpValue a) Source # 

Methods

showsPrec :: Int -> SimpValue a -> ShowS

show :: SimpValue a -> String

showList :: [SimpValue a] -> ShowS

Pretty a => Pretty (SimpValue a) Source # 

compatibleBodies :: Body -> Body -> [Diagnosis] Source #

Check that constants and data type are unchanged and that no axioms was added and no theorem deleted.