equal
deleted
inserted
replaced
16 k = fst c; b = snd c; |
16 k = fst c; b = snd c; |
17 used = fst a; c = snd a |
17 used = fst a; c = snd a |
18 in |
18 in |
19 (! l:used. l < k) & b=c}" |
19 (! l:used. l < k) & b=c}" |
20 |
20 |
21 declare split_paired_All [simp] |
|
22 declare split_paired_Ex [simp del] |
21 declare split_paired_Ex [simp del] |
23 |
22 |
24 |
23 |
25 (* Idea: instead of impl_con_lemma do not rewrite impl_ioa, but derive |
24 (* Idea: instead of impl_con_lemma do not rewrite impl_ioa, but derive |
26 simple lemmas asig_of impl_ioa = impl_sig, trans_of impl_ioa = impl_trans |
25 simple lemmas asig_of impl_ioa = impl_sig, trans_of impl_ioa = impl_trans |