diff -r 78b7010db847 -r 816d8f6513be src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -254,20 +254,20 @@
 by (Force_tac 1);
 qed "delete_map_neq_apply";
 
-(*A set of the form (A Times UNIV) ignores the second (dummy) state component*)
+(*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
 
-Goal "(f o fst) -`` A = (f-``A) Times UNIV";
+Goal "(f o fst) -`` A = (f-``A) <*> UNIV";
 by Auto_tac;
 qed "vimage_o_fst_eq";
 
-Goal "(sub i -``A) Times UNIV = lift_set i (A Times UNIV)";
+Goal "(sub i -``A) <*> UNIV = lift_set i (A <*> UNIV)";
 by Auto_tac;
 qed "vimage_sub_eq_lift_set";
 
 Addsimps [vimage_o_fst_eq, vimage_sub_eq_lift_set];
 
 Goal "[| F : preserves snd;  i~=j |] \
-\     ==> lift j F : stable (lift_set i (A Times UNIV))";
+\     ==> lift j F : stable (lift_set i (A <*> UNIV))";
 by (auto_tac (claset(),
 	      simpset() addsimps [lift_def, lift_set_def, 
 				  stable_def, constrains_def, 
@@ -280,9 +280,9 @@
 
 (*If i~=j then lift j F  does nothing to lift_set i, and the 
   premise ensures A<=B.*)
-Goal "[| F i : (A Times UNIV) co (B Times UNIV);  \
+Goal "[| F i : (A <*> UNIV) co (B <*> UNIV);  \
 \        F j : preserves snd |]  \
-\  ==> lift j (F j) : (lift_set i (A Times UNIV)) co (lift_set i (B Times UNIV))";
+\  ==> lift j (F j) : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))";
 by (case_tac "i=j" 1);
 by (asm_full_simp_tac (simpset() addsimps [lift_def, lift_set_def, 
 					   rename_constrains]) 1);
@@ -323,8 +323,8 @@
 qed "lift_map_eq_diff";
 
 Goal "F : preserves snd \
-\     ==> (lift i F : transient (lift_set j (A Times UNIV))) = \
-\         (i=j & F : transient (A Times UNIV) | A={})";
+\     ==> (lift i F : transient (lift_set j (A <*> UNIV))) = \
+\         (i=j & F : transient (A <*> UNIV) | A={})";
 by (case_tac "i=j" 1);
 by (auto_tac (claset(), simpset() addsimps [lift_transient]));
 by (auto_tac (claset(),
@@ -349,8 +349,8 @@
 qed "lift_transient_eq_disj";
 
 (*USELESS??*)
-Goal "lift_map i `` (A Times UNIV) = \
-\     (UN s:A. UN f. {insert_map i s f}) Times UNIV";
+Goal "lift_map i `` (A <*> UNIV) = \
+\     (UN s:A. UN f. {insert_map i s f}) <*> UNIV";
 by (auto_tac (claset() addSIs [bexI, image_eqI],
               simpset() addsimps [lift_map_def]));
 by (rtac (split RS sym) 1);