equal
deleted
inserted
replaced
1 (* Title: ZF/UNITY/UNITY.thy |
1 (* Title: ZF/UNITY/UNITY.thy |
2 Author: Sidi O Ehmety, Computer Laboratory |
2 Author: Sidi O Ehmety, Computer Laboratory |
3 Copyright 2001 University of Cambridge |
3 Copyright 2001 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 header {*The Basic UNITY Theory*} |
6 section {*The Basic UNITY Theory*} |
7 |
7 |
8 theory UNITY imports State begin |
8 theory UNITY imports State begin |
9 |
9 |
10 text{*The basic UNITY theory (revised version, based upon the "co" operator) |
10 text{*The basic UNITY theory (revised version, based upon the "co" operator) |
11 From Misra, "A Logic for Concurrent Programming", 1994. |
11 From Misra, "A Logic for Concurrent Programming", 1994. |