--- a/src/HOLCF/IOA/meta_theory/TLS.thy Wed Jan 14 11:22:03 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy Wed Jan 14 16:38:04 1998 +0100
@@ -75,6 +75,11 @@
validIOA_def
"validIOA A P == ! ex : executions A . (ex |== P)"
+rules
+
+ex2seq_UUAlt
+ "ex2seq (s,UU) = (s,None,s)>>UU"
+
end