equal
deleted
inserted
replaced
6 More about options |
6 More about options |
7 *) |
7 *) |
8 |
8 |
9 header {* \isaheader{More about Options} *} |
9 header {* \isaheader{More about Options} *} |
10 |
10 |
11 theory Opt = Err: |
11 theory Opt imports Err begin |
12 |
12 |
13 constdefs |
13 constdefs |
14 le :: "'a ord \<Rightarrow> 'a option ord" |
14 le :: "'a ord \<Rightarrow> 'a option ord" |
15 "le r o1 o2 == case o2 of None \<Rightarrow> o1=None | |
15 "le r o1 o2 == case o2 of None \<Rightarrow> o1=None | |
16 Some y \<Rightarrow> (case o1 of None \<Rightarrow> True |
16 Some y \<Rightarrow> (case o1 of None \<Rightarrow> True |