1This directory contains a deep embedding of the Accellera standard
2Property Specification Language (PSL/Sugar) Version 1.1 in HOL. 
3
4The contents of this directory are
5
6README ......................... This file
7SyntaxScript.sml ............... Abstract syntax of core PSL
8ModelScript.sml ................ Theory of models
9ModelLemmasScript.sml .......... Properties of models and automata
10UnclockedSemanticsScript.sml ... Unclocked semantics
11ClockedSemanticsScript.sml ..... Clocked Semantics
12ExtendedSyntaxScript.sml ....... Abstract syntax of full PSL 
13SyntacticSugarScript.sml ....... Semantics of full PSL 
14RewritesScript.sml ............. Rewrites semantics of PSL
15LemmasScript.sml   ............. Some lemmas from Eisner, Fisman, Havlicek
16ProjectionScript.sml............ Validation of the projection view (incomplete)
17
18Also needed is
19
20FinitePSLPathScript.sml ........... Theory of finite paths (lists)
21PSLPathScript.sml ................. Finite and infinite paths
22
23which are in the directory PSL/path 
24(should be ../../path relative to this one).
25
26To run Holmake including the path directory, use:
27
28   Holmake -I ../../path
29
30[MJCG Sun Jan 16 2005: 
31 Fixed to work with type variables introduced by Hol_datatype being in
32 alphabetic order]
33