src/HOLCF/IOA/NTP/Correctness.thy
changeset 26339 7825c83c9eff
parent 25131 2c8caac48ade
child 35174 e15040ae75d7
equal deleted inserted replaced
26338:f8ed02f22433 26339:7825c83c9eff
    12 definition
    12 definition
    13   hom :: "'m impl_state => 'm list" where
    13   hom :: "'m impl_state => 'm list" where
    14   "hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
    14   "hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
    15                          else tl(sq(sen s)))"
    15                          else tl(sq(sen s)))"
    16 
    16 
    17 ML_setup {*
    17 declaration {* fn _ =>
    18 (* repeated from Traces.ML *)
    18   (* repeated from Traces.ML *)
    19 change_claset (fn cs => cs delSWrapper "split_all_tac")
    19   Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")
    20 *}
    20 *}
    21 
    21 
    22 lemmas hom_ioas = Spec.ioa_def Spec.trans_def sender_trans_def receiver_trans_def impl_ioas
    22 lemmas hom_ioas = Spec.ioa_def Spec.trans_def sender_trans_def receiver_trans_def impl_ioas
    23   and impl_asigs = sender_asig_def receiver_asig_def srch_asig_def rsch_asig_def
    23   and impl_asigs = sender_asig_def receiver_asig_def srch_asig_def rsch_asig_def
    24 
    24