1 2This directory contains an experimentation semantics supplied by Johan 3Martensson and (mostly) translated into HOL by Mike Gordon. 4 5 Johan Martensson, PhD Office: +46 31 7451913 6 R&D Mobile: +46 703749681 7 Safelogic AB Fax: +46 31 7451939 8 Arvid Hedvalls Backe 4 johan.martensson@safelogic.se 9 SE-411 33 Gothenburg, SWEDEN 10 PGP key ID A8857A60 11 www.safelogic.se 12 13The file SERE.ml defines the syntax and semantics of regular 14expressions, and proves some properties suggested by Johan. This file 15can be read into HOL with the "use" function. The file SERE.ml.html 16is a version of SERE.ml with HTML in comments. It can be viewed at: 17http://www.cl.cam.ac.uk/~mjcg/PSL/SERE.ml.html 18 19The contents of this directory are 20 21README ................................ This file 22SERE.ml ............................... Syntax and semantics of SEREs 23SERE.ml.html .......................... Version of SERE.ml with HTML comments 24WeakPSLUnclockedSemanticsScript.sml ... Holmake script for separate compilation 25 26To run Holmake including the path directory, use: 27 28 Holmake -I ../path -I ../1.1/official-semantics 29 30Mike Gordon 31Wed Jun 23, 2004 32