--- a/src/HOL/UNITY/Guar.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Guar.thy Sat Sep 23 16:02:01 2000 +0200
@@ -35,11 +35,9 @@
welldef :: 'a program set
"welldef == {F. Init F ~= {}}"
- guar :: ['a program set, 'a=>'b, 'a program set] => 'a program set
- ("(_/ guarantees[_]/ _)" [55,0,55] 55)
- (*higher than membership, lower than Co*)
- "X guarantees[v] Y == {F. ALL G : preserves v.
- F Join G : X --> F Join G : Y}"
+ guar :: ['a program set, 'a program set] => 'a program set
+ (infixl "guarantees" 55) (*higher than membership, lower than Co*)
+ "X guarantees Y == {F. ALL G. F ok G --> F Join G : X --> F Join G : Y}"
refines :: ['a program, 'a program, 'a program set] => bool
("(3_ refines _ wrt _)" [10,10,10] 10)