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)

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

data Body

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

Instances

data TheoryHead

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

Constructors

TheoryHead 

Instances

data SimpValue a

Constructors

SimpValue 

Fields

hasSimp :: Bool
 
simpValue :: a
 

Instances

Eq a => Eq (SimpValue a) 
Show a => Show (SimpValue a) 
Pretty a => Pretty (SimpValue a) 

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

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