equal
deleted
inserted
replaced
68 apply(simp add: expand_fun_eq) |
68 apply(simp add: expand_fun_eq) |
69 apply(simp add: Quotient_abs_rep[OF q]) |
69 apply(simp add: Quotient_abs_rep[OF q]) |
70 done |
70 done |
71 |
71 |
72 lemma option_map_id[id_simps]: |
72 lemma option_map_id[id_simps]: |
73 shows "Option.map id \<equiv> id" |
73 shows "Option.map id = id" |
74 apply (rule eq_reflection) |
|
75 by (simp add: expand_fun_eq split_option_all) |
74 by (simp add: expand_fun_eq split_option_all) |
76 |
75 |
77 lemma option_rel_eq[id_simps]: |
76 lemma option_rel_eq[id_simps]: |
78 shows "option_rel (op =) \<equiv> (op =)" |
77 shows "option_rel (op =) = (op =)" |
79 apply(rule eq_reflection) |
|
80 by (simp add: expand_fun_eq split_option_all) |
78 by (simp add: expand_fun_eq split_option_all) |
81 |
79 |
82 end |
80 end |