diff -r c5a7a7685826 -r 2430ccbde87d src/HOL/UNITY/PPROD.thy
--- a/src/HOL/UNITY/PPROD.thy	Wed Nov 25 15:54:41 1998 +0100
+++ b/src/HOL/UNITY/PPROD.thy	Wed Nov 25 15:55:00 1998 +0100
@@ -7,7 +7,7 @@
 Also merging of state sets.
 *)
 
-PPROD = Union +
+PPROD = Union + Comp +
 
 constdefs
   (*Cartesian product of two relations*)
@@ -22,6 +22,9 @@
 *)
 
 constdefs
+  fst_act :: "(('a*'b) * ('a*'b)) set => ('a*'a) set"
+    "fst_act act == (%((x,y),(x',y')). (x,x')) `` act"
+
   Lcopy :: "'a program => ('a*'b) program"
     "Lcopy F == mk_program (Init F Times UNIV,
 			    (%act. act RTimes Id) `` Acts F)"
@@ -29,12 +32,15 @@
   lift_act :: "['a, ('b*'b) set] => (('a=>'b) * ('a=>'b)) set"
     "lift_act i act == {(f,f'). EX s'. f' = f(i:=s') & (f i, s') : act}"
 
+  drop_act :: "['a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set"
+    "drop_act i act == (%(f,f'). (f i, f' i)) `` act"
+
   lift_prog :: "['a, 'b program] => ('a => 'b) program"
     "lift_prog i F == mk_program ({f. f i : Init F}, lift_act i `` Acts F)"
 
   (*products of programs*)
-  PPROD  :: ['a set, 'b program] => ('a => 'b) program
-    "PPROD I F == JN i:I. lift_prog i F"
+  PPROD  :: ['a set, 'a => 'b program] => ('a => 'b) program
+    "PPROD I F == JN i:I. lift_prog i (F i)"
 
 syntax
   "@PPROD" :: [pttrn, 'a set, 'b set] => ('a => 'b) set ("(3PPI _:_./ _)" 10)