equal
deleted
inserted
replaced
845 |
845 |
846 typedef Pg = "UNIV//eq_game_rel" |
846 typedef Pg = "UNIV//eq_game_rel" |
847 by (auto simp add: quotient_def) |
847 by (auto simp add: quotient_def) |
848 |
848 |
849 lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel" |
849 lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel" |
850 by (auto simp add: equiv_def refl_def sym_def trans_def eq_game_rel_def |
850 by (auto simp add: equiv_def refl_on_def sym_def trans_def eq_game_rel_def |
851 eq_game_sym intro: eq_game_refl eq_game_trans) |
851 eq_game_sym intro: eq_game_refl eq_game_trans) |
852 |
852 |
853 instantiation Pg :: "{ord, zero, plus, minus, uminus}" |
853 instantiation Pg :: "{ord, zero, plus, minus, uminus}" |
854 begin |
854 begin |
855 |
855 |