tuned;
authorwenzelm
Sat Feb 03 17:43:05 2001 +0100 (2001-02-03)
changeset 1104710c51288b00d
parent 11046 b5f5942781a0
child 11048 2f4976370b7a
tuned;
src/HOL/Library/While_Combinator.thy
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Sat Feb 03 17:40:16 2001 +0100
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Sat Feb 03 17:43:05 2001 +0100
     1.3 @@ -114,7 +114,7 @@
     1.4    "[| mono f; finite U; f U = U |] ==>
     1.5      lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
     1.6  apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and
     1.7 -                r = "((Pow U <*> UNIV) <*> (Pow U <*> UNIV)) \<inter>
     1.8 +                r = "((Pow U \<times> UNIV) \<times> (Pow U \<times> UNIV)) \<inter>
     1.9                       inv_image finite_psubset (op - U o fst)" in while_rule)
    1.10     apply (subst lfp_unfold)
    1.11      apply assumption