Modifications for trancl_tac (new solver in simplifier).
authorballarin
Mon Aug 02 10:15:37 2004 +0200 (2004-08-02)
changeset 15097b807858b97bd
parent 15096 be1d3b8cfbd5
child 15098 0726e7b15618
Modifications for trancl_tac (new solver in simplifier).
src/HOL/MicroJava/Comp/CorrComp.thy
src/HOL/MicroJava/J/WellForm.thy
src/HOL/UNITY/Simple/Reach.thy
     1.1 --- a/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Aug 02 10:12:02 2004 +0200
     1.2 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Aug 02 10:15:37 2004 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4  done
     1.5  
     1.6  theorem exec_all_refl: "exec_all G s s"
     1.7 -by (simp only: exec_all_def (* CBtrancl, rule rtrancl_refl*) )
     1.8 +by (simp only: exec_all_def)
     1.9  
    1.10  
    1.11  theorem exec_instr_in_exec_all:
     2.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Mon Aug 02 10:12:02 2004 +0200
     2.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Mon Aug 02 10:15:37 2004 +0200
     2.3 @@ -316,7 +316,6 @@
     2.4  apply(  assumption)
     2.5  apply( fast)
     2.6  apply(auto dest!: wf_cdecl_supD)
     2.7 -(*CBtrancl: apply(erule (1) converse_rtrancl_into_rtrancl) *)
     2.8  done
     2.9  
    2.10  lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT"
     3.1 --- a/src/HOL/UNITY/Simple/Reach.thy	Mon Aug 02 10:12:02 2004 +0200
     3.2 +++ b/src/HOL/UNITY/Simple/Reach.thy	Mon Aug 02 10:15:37 2004 +0200
     3.3 @@ -75,7 +75,6 @@
     3.4  apply (unfold fixedpoint_def)
     3.5  apply (rule equalityI)
     3.6  apply (auto intro!: ext)
     3.7 -(* CBtrancl: prefer 2 apply (blast intro: rtrancl_trans) *)
     3.8  apply (erule rtrancl_induct, auto)
     3.9  done
    3.10