--- a/src/HOL/ZF/Games.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/ZF/Games.thy Fri Jun 26 10:20:33 2015 +0200
@@ -831,10 +831,10 @@
Pg_less_def: "G < H \<longleftrightarrow> G \<le> H \<and> G \<noteq> (H::Pg)"
definition
- Pg_minus_def: "- G = the_elem (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
+ Pg_minus_def: "- G = the_elem (\<Union>g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
definition
- 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})})"
+ 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})})"
definition
Pg_diff_def: "G - H = G + (- (H::Pg))"