This directory contains a deep embedding of the Accellera standard
Property Specification Language (PSL/Sugar) Version 1.1 in HOL. 

The contents of this directory are

README ......................... This file
SyntaxScript.sml ............... Abstract syntax of core PSL
ModelScript.sml ................ Theory of models
ModelLemmasScript.sml .......... Properties of models and automata
UnclockedSemanticsScript.sml ... Unclocked semantics
ClockedSemanticsScript.sml ..... Clocked Semantics
ExtendedSyntaxScript.sml ....... Abstract syntax of full PSL 
SyntacticSugarScript.sml ....... Semantics of full PSL 
RewritesScript.sml ............. Rewrites semantics of PSL
LemmasScript.sml   ............. Some lemmas from Eisner, Fisman, Havlicek
ProjectionScript.sml............ Validation of the projection view (incomplete)

Also needed is

FinitePSLPathScript.sml ........... Theory of finite paths (lists)
PSLPathScript.sml ................. Finite and infinite paths

which are in the directory PSL/path 
(should be ../../path relative to this one).

To run Holmake including the path directory, use:

   Holmake -I ../../path

[MJCG Sun Jan 16 2005: 
 Fixed to work with type variables introduced by Hol_datatype being in
 alphabetic order]