--- a/src/HOL/UNITY/Channel.thy Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Channel.thy Thu Oct 15 11:35:07 1998 +0200
@@ -12,18 +12,19 @@
types state = nat set
+consts
+ F :: state program
+
constdefs
minSet :: nat set => nat option
"minSet A == if A={} then None else Some (LEAST x. x:A)"
rules
- skip "Id: acts"
-
- UC1 "constrains acts (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))"
+ UC1 "F : constrains (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))"
- (* UC1 "constrains acts {s. minSet s = x} {s. x <= minSet s}" *)
+ (* UC1 "F : constrains {s. minSet s = x} {s. x <= minSet s}" *)
- UC2 "leadsTo acts (minSet -`` {Some x}) {s. x ~: s}"
+ UC2 "F : leadsTo (minSet -`` {Some x}) {s. x ~: s}"
end