This directory contains an experimentation semantics supplied by Johan
Martensson and (mostly) translated into HOL by Mike Gordon.

 Johan Martensson, PhD            Office: +46 31 7451913
 R&D                              Mobile: +46 703749681
 Safelogic AB                     Fax: +46 31 7451939
 Arvid Hedvalls Backe 4           johan.martensson@safelogic.se
 SE-411 33 Gothenburg, SWEDEN
 PGP key ID A8857A60
 www.safelogic.se

The file SERE.ml defines the syntax and semantics of regular
expressions, and proves some properties suggested by Johan. This file
can be read into HOL with the "use" function.  The file SERE.ml.html
is a version of SERE.ml with HTML in comments. It can be viewed at:
http://www.cl.cam.ac.uk/~mjcg/PSL/SERE.ml.html

The contents of this directory are

README ................................ This file
SERE.ml ............................... Syntax and semantics of SEREs
SERE.ml.html .......................... Version of SERE.ml with HTML comments
WeakPSLUnclockedSemanticsScript.sml ... Holmake script for separate compilation

To run Holmake including the path directory, use:

   Holmake -I ../path -I ../1.1/official-semantics

Mike Gordon
Wed Jun 23, 2004