src/HOLCF/IOA/meta_theory/LiveIOA.thy
changeset 35215 a03462cbf86f
parent 35174 e15040ae75d7
child 36452 d37c6eed8117
     1.1 --- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Thu Feb 18 12:36:09 2010 -0800
     1.2 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Thu Feb 18 13:29:59 2010 -0800
     1.3 @@ -43,8 +43,6 @@
     1.4                                             ((corresp_ex (fst AM) f exec) |== (snd AM))))"
     1.5  
     1.6  
     1.7 -declare split_paired_Ex [simp del]
     1.8 -
     1.9  lemma live_implements_trans:
    1.10  "!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |]
    1.11        ==> live_implements (A,LA) (C,LC)"