--- a/src/ZF/UNITY/Comp.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/Comp.thy Tue May 27 11:39:03 2003 +0200
@@ -15,7 +15,7 @@
*)
-Comp = Union +
+Comp = Union + Increasing +
constdefs
@@ -36,9 +36,12 @@
preserves :: (i=>i)=>i
"preserves(f) == {F:program. ALL z. F: stable({s:state. f(s) = z})}"
+ fun_pair :: "[i=>i, i =>i] =>(i=>i)"
+ "fun_pair(f, g) == %x. <f(x), g(x)>"
+
localize :: "[i=>i, i] => i"
"localize(f,F) == mk_program(Init(F), Acts(F),
- AllowedActs(F) Int (UN G:preserves(f). Acts(G)))"
+ AllowedActs(F) Int (UN G:preserves(f). Acts(G)))"
end