equal
deleted
inserted
replaced
27 val prems = goalw Rel.thy [sym_def] |
27 val prems = goalw Rel.thy [sym_def] |
28 "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)"; |
28 "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)"; |
29 by (REPEAT (ares_tac (prems @ [allI,impI]) 1)); |
29 by (REPEAT (ares_tac (prems @ [allI,impI]) 1)); |
30 qed "symI"; |
30 qed "symI"; |
31 |
31 |
32 Goalw [sym_def] "!!r. [| sym(r); <x,y>: r |] ==> <y,x>: r"; |
32 Goalw [sym_def] "[| sym(r); <x,y>: r |] ==> <y,x>: r"; |
33 by (Blast_tac 1); |
33 by (Blast_tac 1); |
34 qed "symE"; |
34 qed "symE"; |
35 |
35 |
36 (* antisymmetry *) |
36 (* antisymmetry *) |
37 |
37 |