A few lemmas and some Adds.

--- a/src/HOL/Relation.ML	Sun Feb 20 09:32:06 2000 +0100
+++ b/src/HOL/Relation.ML	Mon Feb 21 10:20:38 2000 +0100
@@ -21,7 +21,7 @@
 Goalw [Id_def] "(a,b):Id = (a=b)";
 by (Blast_tac 1);
 qed "pair_in_Id_conv";
-Addsimps [pair_in_Id_conv];
+AddIffs [pair_in_Id_conv];
 
 Goalw [refl_def] "reflexive Id";
 by Auto_tac;

--- a/src/HOL/Trancl.ML	Sun Feb 20 09:32:06 2000 +0100
+++ b/src/HOL/Trancl.ML	Mon Feb 21 10:20:38 2000 +0100
@@ -142,6 +142,17 @@
 qed "rtrancl_reflcl";
 Addsimps [rtrancl_reflcl];
 
+Goal "(r - Id)^* = r^*";
+br sym 1;
+br rtrancl_subset 1;
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by(rename_tac "a b" 1);
+by(case_tac "a=b" 1);
+ by (Blast_tac 1);
+by(blast_tac (claset() addSIs [r_into_rtrancl]) 1);
+qed "rtrancl_r_diff_Id";
+
 Goal "(x,y) : (r^-1)^* ==> (x,y) : (r^*)^-1";
 by (rtac converseI 1);
 by (etac rtrancl_induct 1);
@@ -347,10 +358,7 @@
 Goal "(r^+)^= = r^*";
 by Safe_tac;
 by  (etac trancl_into_rtrancl 1);
-by (etac rtranclE 1);
-by  (Auto_tac );
-by (etac rtrancl_into_trancl1 1);
-by (assume_tac 1);
+by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1);
 qed "reflcl_trancl";
 Addsimps[reflcl_trancl];
 

--- a/src/HOL/WF.ML	Sun Feb 20 09:32:06 2000 +0100
+++ b/src/HOL/WF.ML	Mon Feb 21 10:20:38 2000 +0100
@@ -230,6 +230,19 @@
 Goalw [acyclic_def] "acyclic(r^-1) = acyclic r";
 by (simp_tac (simpset() addsimps [trancl_converse]) 1);
 qed "acyclic_converse";
+AddIffs [acyclic_converse];
+
+Goalw [acyclic_def,antisym_def] "acyclic r ==> antisym(r^*)";
+by(blast_tac (claset() addEs [rtranclE]
+     addIs [rtrancl_into_trancl1,rtrancl_trancl_trancl]) 1);
+qed "acyclic_impl_antisym_rtrancl";
+
+(* Other direction:
+acyclic = no loops
+antisym = only self loops
+Goalw [acyclic_def,antisym_def] "antisym(r^* ) ==> acyclic(r - Id)";
+==> "antisym(r^* ) = acyclic(r - Id)";
+*)
 
 Goalw [acyclic_def] "[| acyclic s; r <= s |] ==> acyclic r";
 by (blast_tac (claset() addIs [trancl_mono]) 1);