--- a/src/HOL/Transitive_Closure_lemmas.ML Mon Jan 29 22:25:45 2001 +0100
+++ b/src/HOL/Transitive_Closure_lemmas.ML Mon Jan 29 23:02:21 2001 +0100
@@ -365,42 +365,3 @@
Goalw [trancl_def] "r <= A <*> A ==> r^+ <= A <*> A";
by (blast_tac (claset() addSDs [lemma]) 1);
qed "trancl_subset_Sigma";
-
-
-Goal "(r^+)^= = r^*";
-by Safe_tac;
-by (etac trancl_into_rtrancl 1);
-by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1);
-qed "reflcl_trancl";
-Addsimps[reflcl_trancl];
-
-Goal "(r^=)^+ = r^*";
-by Safe_tac;
-by (dtac trancl_into_rtrancl 1);
-by (Asm_full_simp_tac 1);
-by (etac rtranclE 1);
-by Safe_tac;
-by (rtac r_into_trancl 1);
-by (Simp_tac 1);
-by (rtac rtrancl_into_trancl1 1);
-by (etac (rtrancl_reflcl RS equalityD2 RS subsetD) 1);
-by (Fast_tac 1);
-qed "trancl_reflcl";
-Addsimps[trancl_reflcl];
-
-Goal "{}^+ = {}";
-by (auto_tac (claset() addEs [trancl_induct], simpset()));
-qed "trancl_empty";
-Addsimps[trancl_empty];
-
-Goal "{}^* = Id";
-by (rtac (reflcl_trancl RS subst) 1);
-by (Simp_tac 1);
-qed "rtrancl_empty";
-Addsimps[rtrancl_empty];
-
-Goal "(a,b):R^* ==> a=b | a~=b & (a,b):R^+";
-by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym]
- delsimps [reflcl_trancl]) 1);
-qed "rtranclD";
-