Modifications for trancl_tac (new solver in simplifier).

--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Aug 02 10:12:02 2004 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Aug 02 10:15:37 2004 +0200
@@ -52,7 +52,7 @@
 done
 
 theorem exec_all_refl: "exec_all G s s"
-by (simp only: exec_all_def (* CBtrancl, rule rtrancl_refl*) )
+by (simp only: exec_all_def)
 
 
 theorem exec_instr_in_exec_all:

--- a/src/HOL/MicroJava/J/WellForm.thy	Mon Aug 02 10:12:02 2004 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy	Mon Aug 02 10:15:37 2004 +0200
@@ -316,7 +316,6 @@
 apply(  assumption)
 apply( fast)
 apply(auto dest!: wf_cdecl_supD)
-(*CBtrancl: apply(erule (1) converse_rtrancl_into_rtrancl) *)
 done
 
 lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT"

--- a/src/HOL/UNITY/Simple/Reach.thy	Mon Aug 02 10:12:02 2004 +0200
+++ b/src/HOL/UNITY/Simple/Reach.thy	Mon Aug 02 10:15:37 2004 +0200
@@ -75,7 +75,6 @@
 apply (unfold fixedpoint_def)
 apply (rule equalityI)
 apply (auto intro!: ext)
-(* CBtrancl: prefer 2 apply (blast intro: rtrancl_trans) *)
 apply (erule rtrancl_induct, auto)
 done