# HG changeset patch
# User wenzelm
# Date 1004747957 -3600
# Node ID 52aa183c15bbb4fbcf06099fc50978dcb3c3f34a
# Parent  1281e9bf57f689bf2373e00d7e05854061ff76b6
replaced Undef by UU;

diff -r 1281e9bf57f6 -r 52aa183c15bb src/HOLCF/IOA/meta_theory/CompoScheds.ML
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Sat Nov 03 01:38:39 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Sat Nov 03 01:39:17 2001 +0100
@@ -26,27 +26,27 @@
 \      nil => nil \
 \   | x##xs => \
 \     (case x of  \
-\       Undef => UU   \
+\       UU => UU   \
 \     | Def y =>  \
 \        (if y:act A then \
 \            (if y:act B then \
 \               (case HD$exA of \
-\                  Undef => UU \
+\                  UU => UU \
 \                | Def a => (case HD$exB of \
-\                             Undef => UU \
+\                             UU => UU \
 \                           | Def b => \
 \                  (y,(snd a,snd b))>>  \
 \                    (mkex2 A B$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))  \
 \             else   \
 \               (case HD$exA of   \
-\                  Undef => UU  \
+\                  UU => UU  \
 \                | Def a => \
 \                  (y,(snd a,t))>>(mkex2 A B$xs$(TL$exA)$exB) (snd a) t)  \
 \             )  \       
 \         else   \
 \            (if y:act B then \
 \               (case HD$exB of  \
-\                  Undef => UU  \
+\                  UU => UU  \
 \                | Def b =>  \
 \                  (y,(s,snd b))>>(mkex2 A B$xs$exA$(TL$exB)) s (snd b))  \
 \            else  \
diff -r 1281e9bf57f6 -r 52aa183c15bb src/HOLCF/IOA/meta_theory/CompoScheds.thy
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Sat Nov 03 01:38:39 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Sat Nov 03 01:39:17 2001 +0100
@@ -33,27 +33,27 @@
        nil => nil
     | x##xs => 
       (case x of 
-        Undef => UU
+        UU => UU
       | Def y => 
          (if y:act A then 
              (if y:act B then 
                 (case HD$exA of
-                   Undef => UU
+                   UU => UU
                  | Def a => (case HD$exB of
-                              Undef => UU
+                              UU => UU
                             | Def b => 
                    (y,(snd a,snd b))>>
                      (h$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
               else
                 (case HD$exA of
-                   Undef => UU
+                   UU => UU
                  | Def a => 
                    (y,(snd a,t))>>(h$xs$(TL$exA)$exB) (snd a) t)
               )
           else 
              (if y:act B then 
                 (case HD$exB of
-                   Undef => UU
+                   UU => UU
                  | Def b => 
                    (y,(s,snd b))>>(h$xs$exA$(TL$exB)) s (snd b))
              else
diff -r 1281e9bf57f6 -r 52aa183c15bb src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Sat Nov 03 01:38:39 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Sat Nov 03 01:39:17 2001 +0100
@@ -12,15 +12,12 @@
                    section "mksch rewrite rules";
 (* ---------------------------------------------------------------- *)
 
-
-
-
 bind_thm ("mksch_unfold", fix_prover2 thy mksch_def 
 "mksch A B = (LAM tr schA schB. case tr of \
 \       nil => nil\
 \    | x##xs => \
 \      (case x of  \ 
-\        Undef => UU  \
+\        UU => UU  \
 \      | Def y => \
 \         (if y:act A then \
 \             (if y:act B then \ 
diff -r 1281e9bf57f6 -r 52aa183c15bb src/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Sat Nov 03 01:38:39 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Sat Nov 03 01:39:17 2001 +0100
@@ -21,7 +21,7 @@
        nil => nil
     | x##xs => 
       (case x of 
-        Undef => UU
+        UU => UU
       | Def y => 
          (if y:act A then 
              (if y:act B then 
diff -r 1281e9bf57f6 -r 52aa183c15bb src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Sat Nov 03 01:38:39 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Sat Nov 03 01:39:17 2001 +0100
@@ -151,9 +151,9 @@
 \             | x##xs => (case t2 of \ 
 \                          nil => UU  \
 \                        | y##ys => (case x of \
-\                                      Undef  => UU \
+\                                      UU  => UU \
 \                                    | Def a => (case y of \
-\                                                  Undef => UU \
+\                                                  UU => UU \
 \                                                | Def b => Def (a,b)##(Zip$xs$ys)))))";
 by (rtac trans 1);
 by (rtac fix_eq2 1);
diff -r 1281e9bf57f6 -r 52aa183c15bb src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Sat Nov 03 01:38:39 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Sat Nov 03 01:39:17 2001 +0100
@@ -73,14 +73,14 @@
              | x##xs => (case t2 of 
                           nil => UU 
                         | y##ys => (case x of 
-                                      Undef  => UU
+                                      UU  => UU
                                     | Def a => (case y of 
-                                                  Undef => UU
+                                                  UU => UU
                                                 | Def b => Def (a,b)##(h$xs$ys))))))"
 
 Filter2_def    "Filter2 P == (fix$(LAM h t. case t of 
             nil => nil
-	  | x##xs => (case x of Undef => UU | Def y => (if P y                                 
+	  | x##xs => (case x of UU => UU | Def y => (if P y                                 
                      then x##(h$xs)
                      else     h$xs))))" 
 
diff -r 1281e9bf57f6 -r 52aa183c15bb src/HOLCF/IOA/meta_theory/ShortExecutions.ML
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Sat Nov 03 01:38:39 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Sat Nov 03 01:39:17 2001 +0100
@@ -28,7 +28,7 @@
 \       nil => nil\
 \    | x##xs => \
 \      (case x of\ 
-\        Undef => UU\
+\        UU => UU\
 \      | Def y => (Takewhile (%a.~ P a)$s)\
 \                  @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$xs))\
 \      )\
diff -r 1281e9bf57f6 -r 52aa183c15bb src/HOLCF/IOA/meta_theory/ShortExecutions.thy
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Sat Nov 03 01:38:39 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Sat Nov 03 01:39:17 2001 +0100
@@ -38,7 +38,7 @@
        nil => nil
     | x##xs => 
       (case x of 
-        Undef => UU
+        UU => UU
       | Def y => (Takewhile (%x.~P x)$s)
                   @@ (y>>(h$(TL$(Dropwhile (%x.~ P x)$s))$xs))
       )
diff -r 1281e9bf57f6 -r 52aa183c15bb src/HOLCF/IOA/meta_theory/TL.thy
--- a/src/HOLCF/IOA/meta_theory/TL.thy	Sat Nov 03 01:38:39 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/TL.thy	Sat Nov 03 01:39:17 2001 +0100
@@ -45,7 +45,7 @@
 
 unlift_def
   "unlift x == (case x of 
-                 Undef   => arbitrary
+                 UU   => arbitrary
                | Def y   => y)"
 
 (* this means that for nil and UU the effect is unpredictable *)
diff -r 1281e9bf57f6 -r 52aa183c15bb src/HOLCF/IOA/meta_theory/Traces.thy
--- a/src/HOLCF/IOA/meta_theory/Traces.thy	Sat Nov 03 01:38:39 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Sat Nov 03 01:39:17 2001 +0100
@@ -125,7 +125,7 @@
 
 laststate_def
   "laststate ex == case Last$(snd ex) of
-                      Undef  => fst ex
+                      UU  => fst ex
                     | Def at => snd at"
 
 inf_often_def