src/HOL/ZF/Games.thy
changeset 39910 10097e0a9dbd
parent 39302 d7728f65b353
child 40824 f5a0cb45d2a5
     1.1 --- a/src/HOL/ZF/Games.thy	Fri Oct 01 14:15:49 2010 +0200
     1.2 +++ b/src/HOL/ZF/Games.thy	Fri Oct 01 16:05:25 2010 +0200
     1.3 @@ -859,10 +859,10 @@
     1.4    Pg_less_def: "G < H \<longleftrightarrow> G \<le> H \<and> G \<noteq> (H::Pg)"
     1.5  
     1.6  definition
     1.7 -  Pg_minus_def: "- G = contents (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
     1.8 +  Pg_minus_def: "- G = the_elem (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
     1.9  
    1.10  definition
    1.11 -  Pg_plus_def: "G + H = contents (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
    1.12 +  Pg_plus_def: "G + H = the_elem (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
    1.13  
    1.14  definition
    1.15    Pg_diff_def: "G - H = G + (- (H::Pg))"