# HG changeset patch
# User ballarin
# Date 1091434537 -7200
# Node ID b807858b97bddaa6cf6206ab833ba5714b3828c4
# Parent  be1d3b8cfbd5cc3c0b92af16f0d2a879838239d1
Modifications for trancl_tac (new solver in simplifier).

diff -r be1d3b8cfbd5 -r b807858b97bd src/HOL/MicroJava/Comp/CorrComp.thy
--- 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:
diff -r be1d3b8cfbd5 -r b807858b97bd src/HOL/MicroJava/J/WellForm.thy
--- 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"
diff -r be1d3b8cfbd5 -r b807858b97bd src/HOL/UNITY/Simple/Reach.thy
--- 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