# HG changeset patch
# User wenzelm
# Date 981218585 -3600
# Node ID 10c51288b00d6b4015bb8276698abb3f0be2fb3e
# Parent  b5f5942781a068105d8cb23634e99ee04471df01
tuned;

diff -r b5f5942781a0 -r 10c51288b00d src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Sat Feb 03 17:40:16 2001 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Sat Feb 03 17:43:05 2001 +0100
@@ -114,7 +114,7 @@
   "[| mono f; finite U; f U = U |] ==>
     lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
 apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and
-                r = "((Pow U <*> UNIV) <*> (Pow U <*> UNIV)) \<inter>
+                r = "((Pow U \<times> UNIV) \<times> (Pow U \<times> UNIV)) \<inter>
                      inv_image finite_psubset (op - U o fst)" in while_rule)
    apply (subst lfp_unfold)
     apply assumption