--- 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 \
--- 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
--- 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 \
--- 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
--- 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);
--- 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))))"
--- 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))\
\ )\
--- 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))
)
--- 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 *)
--- 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