equal
deleted
inserted
replaced
40 by (forward_tac prems 3); |
40 by (forward_tac prems 3); |
41 by Auto_tac; |
41 by Auto_tac; |
42 qed "option_caseE"; |
42 qed "option_caseE"; |
43 |
43 |
44 |
44 |
45 section "the"; |
|
46 |
|
47 Goalw [the_def] "the (Some x) = x"; |
|
48 by (Simp_tac 1); |
|
49 qed "the_Some"; |
|
50 |
|
51 Addsimps [the_Some]; |
|
52 |
|
53 |
|
54 |
|
55 section "option_map"; |
45 section "option_map"; |
56 |
46 |
57 Goalw [option_map_def] "option_map f None = None"; |
47 Goalw [option_map_def] "option_map f None = None"; |
58 by (Simp_tac 1); |
48 by (Simp_tac 1); |
59 qed "option_map_None"; |
49 qed "option_map_None"; |