# HG changeset patch
# User paulson
# Date 932999378 -7200
# Node ID 9663eb2bce05c88b19697e18c252478aec509785
# Parent  f444e632cdf58d49fb09d3792d6a18b5e360f1ba
three new theorems

diff -r f444e632cdf5 -r 9663eb2bce05 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Mon Jul 26 16:08:15 1999 +0200
+++ b/src/HOL/Relation.ML	Mon Jul 26 16:29:38 1999 +0200
@@ -4,8 +4,6 @@
     Copyright   1996  University of Cambridge
 *)
 
-open Relation;
-
 (** Identity relation **)
 
 Goalw [Id_def] "(a,a) : Id";  
@@ -201,6 +199,18 @@
 qed "converse_diag";
 Addsimps [converse_diag];
 
+Goalw [refl_def] "refl A r ==> refl A (converse r)";
+by (Blast_tac 1);
+qed "refl_converse";
+
+Goalw [antisym_def] "antisym (converse r) = antisym r";
+by (Blast_tac 1);
+qed "antisym_converse";
+
+Goalw [trans_def] "trans (converse r) = trans r";
+by (Blast_tac 1);
+qed "trans_converse";
+
 (** Domain **)
 
 Goalw [Domain_def] "a: Domain(r) = (EX y. (a,y): r)";