equal
deleted
inserted
replaced
78 apply(rule equivp_transp[OF a]) |
78 apply(rule equivp_transp[OF a]) |
79 apply(assumption)+ |
79 apply(assumption)+ |
80 apply(simp only: option_rel_some[OF a]) |
80 apply(simp only: option_rel_some[OF a]) |
81 done |
81 done |
82 |
82 |
|
83 lemma option_map_id[id_simps]: "option_map id \<equiv> id" |
|
84 apply (rule eq_reflection) |
|
85 apply (rule ext) |
|
86 apply (case_tac x) |
|
87 apply (auto) |
|
88 done |
|
89 |
|
90 lemma option_rel_eq[id_simps]: "option_rel op = \<equiv> op =" |
|
91 apply (rule eq_reflection) |
|
92 apply (rule ext)+ |
|
93 apply (case_tac x) |
|
94 apply auto |
|
95 apply (case_tac xa) |
|
96 apply auto |
|
97 apply (case_tac xa) |
|
98 apply auto |
|
99 done |
|
100 |
83 end |
101 end |