equal
deleted
inserted
replaced
9 begin |
9 begin |
10 |
10 |
11 datatype_new 'a option = |
11 datatype_new 'a option = |
12 None |
12 None |
13 | Some (the: 'a) |
13 | Some (the: 'a) |
|
14 |
14 datatype_compat option |
15 datatype_compat option |
15 |
16 |
16 lemma [case_names None Some, cases type: option]: |
17 lemma [case_names None Some, cases type: option]: |
17 -- {* for backward compatibility -- names of variables differ *} |
18 -- {* for backward compatibility -- names of variables differ *} |
18 "(y = None \<Longrightarrow> P) \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> P) \<Longrightarrow> P" |
19 "(y = None \<Longrightarrow> P) \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> P) \<Longrightarrow> P" |