# HG changeset patch
# User nipkow
# Date 1380747936 -7200
# Node ID f6bd38fb2c395cb0c80366872b634b35aec4c5b3
# Parent  16374631b5047144970e4f12eb111cb06ffc00d7# Parent  83fb090dae9ecdf973ecd29bbdd3003429c2c889
merged

diff -r 16374631b504 -r f6bd38fb2c39 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Wed Oct 02 22:59:54 2013 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Wed Oct 02 23:05:36 2013 +0200
@@ -1,7 +1,6 @@
 (*  Title:      HOL/Library/While_Combinator.thy
     Author:     Tobias Nipkow
     Author:     Alexander Krauss
-    Copyright   2000 TU Muenchen
 *)
 
 header {* A general ``while'' combinator *}
@@ -257,7 +256,7 @@
   while_option (%(ws,_). ws \<noteq> [] \<and> p(hd ws))
     ((%(ws,Z).
      let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x)
-     in (new @ tl ws, set new \<union> insert x Z)))
+     in (new @ tl ws, set new \<union> Z)))
     ([x],{x})"
 
 lemma rtrancl_while_Some: assumes "rtrancl_while p f x = Some(ws,Z)"
@@ -268,7 +267,7 @@
   let ?test = "(%(ws,_). ws \<noteq> [] \<and> p(hd ws))"
   let ?step = "(%(ws,Z).
      let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x)
-     in (new @ tl ws, set new \<union> insert x Z))"
+     in (new @ tl ws, set new \<union> Z))"
   let ?R = "{(x,y). y \<in> set(f x)}"
   let ?Inv = "%(ws,Z). x \<in> Z \<and> set ws \<subseteq> Z \<and> ?R `` (Z - set ws) \<subseteq> Z \<and>
                        Z \<subseteq> ?R^* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z)"