src/HOLCF/IOA/ABP/Lemmas.ML
changeset 3852 e694c660055b
parent 3072 a31419014be5
child 4098 71e05eb27fb6
     1.1 --- a/src/HOLCF/IOA/ABP/Lemmas.ML	Mon Oct 13 12:48:42 1997 +0200
     1.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Mon Oct 13 12:51:51 1997 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  
     1.5  (* 2 Lemmas to add to set_lemmas ... , used also for action handling, 
     1.6     namely for Intersections and the empty list (compatibility of IOA!)  *)
     1.7 -goal Set.thy "(UN b.{x.x=f(b)})= (UN b.{f(b)})"; 
     1.8 +goal Set.thy "(UN b.{x. x=f(b)})= (UN b.{f(b)})"; 
     1.9   by (rtac set_ext 1);
    1.10   by (Fast_tac 1);
    1.11  val singleton_set =result();