| changeset 5137 | 60205b0de9b9 |
| parent 5067 | 62b6288e6005 |
| child 5147 | 825877190618 |
--- a/src/ZF/Rel.ML Mon Jul 13 16:42:27 1998 +0200 +++ b/src/ZF/Rel.ML Mon Jul 13 16:43:57 1998 +0200 @@ -29,7 +29,7 @@ by (REPEAT (ares_tac (prems @ [allI,impI]) 1)); qed "symI"; -Goalw [sym_def] "!!r. [| sym(r); <x,y>: r |] ==> <y,x>: r"; +Goalw [sym_def] "[| sym(r); <x,y>: r |] ==> <y,x>: r"; by (Blast_tac 1); qed "symE";