src/HOL/Library/While_Combinator.thy
changeset 54047 83fb090dae9e
parent 53381 355a4cac5440
child 54050 48c800d8ba2d
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Wed Oct 02 19:49:31 2013 +0200
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Wed Oct 02 22:32:50 2013 +0200
     1.3 @@ -1,7 +1,6 @@
     1.4  (*  Title:      HOL/Library/While_Combinator.thy
     1.5      Author:     Tobias Nipkow
     1.6      Author:     Alexander Krauss
     1.7 -    Copyright   2000 TU Muenchen
     1.8  *)
     1.9  
    1.10  header {* A general ``while'' combinator *}
    1.11 @@ -257,7 +256,7 @@
    1.12    while_option (%(ws,_). ws \<noteq> [] \<and> p(hd ws))
    1.13      ((%(ws,Z).
    1.14       let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x)
    1.15 -     in (new @ tl ws, set new \<union> insert x Z)))
    1.16 +     in (new @ tl ws, set new \<union> Z)))
    1.17      ([x],{x})"
    1.18  
    1.19  lemma rtrancl_while_Some: assumes "rtrancl_while p f x = Some(ws,Z)"
    1.20 @@ -268,7 +267,7 @@
    1.21    let ?test = "(%(ws,_). ws \<noteq> [] \<and> p(hd ws))"
    1.22    let ?step = "(%(ws,Z).
    1.23       let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x)
    1.24 -     in (new @ tl ws, set new \<union> insert x Z))"
    1.25 +     in (new @ tl ws, set new \<union> Z))"
    1.26    let ?R = "{(x,y). y \<in> set(f x)}"
    1.27    let ?Inv = "%(ws,Z). x \<in> Z \<and> set ws \<subseteq> Z \<and> ?R `` (Z - set ws) \<subseteq> Z \<and>
    1.28                         Z \<subseteq> ?R^* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z)"