equal
deleted
inserted
replaced
80 apply (case_tac x) |
80 apply (case_tac x) |
81 apply (auto) |
81 apply (auto) |
82 done |
82 done |
83 |
83 |
84 lemma option_rel_eq[id_simps]: |
84 lemma option_rel_eq[id_simps]: |
85 shows "option_rel op = \<equiv> op =" |
85 shows "option_rel (op =) \<equiv> (op =)" |
86 apply(rule eq_reflection) |
86 apply(rule eq_reflection) |
87 apply(auto simp add: expand_fun_eq) |
87 apply(auto simp add: expand_fun_eq) |
88 apply(case_tac x) |
88 apply(case_tac x) |
89 apply(case_tac [!] xa) |
89 apply(case_tac [!] xa) |
90 apply(auto) |
90 apply(auto) |