--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/UNITY.thy Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,27 @@
+(* Title: HOL/UNITY/UNITY
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+The basic UNITY theory (revised version, based upon the "co" operator)
+
+From Misra, "A Logic for Concurrent Programming", 1994
+*)
+
+UNITY = LessThan +
+
+constdefs
+
+ constrains :: "[('a * 'a)set set, 'a set, 'a set] => bool"
+ "constrains Acts A B == ALL act:Acts. act^^A <= B"
+
+ stable :: "('a * 'a)set set => 'a set => bool"
+ "stable Acts A == constrains Acts A A"
+
+ strongest_rhs :: "[('a * 'a)set set, 'a set] => 'a set"
+ "strongest_rhs Acts A == Inter {B. constrains Acts A B}"
+
+ unless :: "[('a * 'a)set set, 'a set, 'a set] => bool"
+ "unless mutex A B == constrains mutex (A-B) (A Un B)"
+
+end