# HG changeset patch
# User paulson
# Date 905440996 -7200
# Node ID 08ca6e067ee6ccb67d1afcf21440025ff5fe1c0b
# Parent  fe9d103464a4b48b292b69ce47a9f154805e19d4
tided the unused rule irrefl_tranclI

diff -r fe9d103464a4 -r 08ca6e067ee6 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Thu Sep 10 17:20:49 1998 +0200
+++ b/src/HOL/Trancl.ML	Thu Sep 10 17:23:16 1998 +0200
@@ -293,17 +293,18 @@
 
 Goalw [trancl_def] "(r^-1)^+ = (r^+)^-1";
 by (simp_tac (simpset() addsimps [rtrancl_converse,converse_comp]) 1);
-by (simp_tac (simpset() addsimps [rtrancl_converse RS sym,r_comp_rtrancl_eq])1);
+by (simp_tac (simpset() addsimps [rtrancl_converse RS sym,
+				  r_comp_rtrancl_eq]) 1);
 qed "trancl_converse";
 
-val irrefl_tranclI = prove_goal Trancl.thy 
-	"!!r. r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+" (K [
-	rtac allI 1,
-	subgoal_tac "!y. (x, y) : r^+ --> x~=y" 1,
-	 Fast_tac 1,
-	strip_tac 1,
-	etac trancl_induct 1,
-	 auto_tac (claset() addEs [equals0E, r_into_trancl], simpset())]);
+(*Unused*)
+qed_goal "irrefl_tranclI" Trancl.thy 
+   "!!r. r^-1 Int r^+ = {} ==> (x, x) ~: r^+" 
+ (K [subgoal_tac "!y. (x, y) : r^+ --> x~=y" 1,
+     Fast_tac 1,
+     strip_tac 1,
+     etac trancl_induct 1,
+     auto_tac (claset() addIs [r_into_trancl], simpset())]);
 
 Goal "[| (a,b) : r^*;  r <= A Times A |] ==> a=b | a:A";
 by (etac rtrancl_induct 1);