equal
deleted
inserted
replaced
6 The error type |
6 The error type |
7 *) |
7 *) |
8 |
8 |
9 header {* \isaheader{The Error Type} *} |
9 header {* \isaheader{The Error Type} *} |
10 |
10 |
11 theory Err = Semilat: |
11 theory Err imports Semilat begin |
12 |
12 |
13 datatype 'a err = Err | OK 'a |
13 datatype 'a err = Err | OK 'a |
14 |
14 |
15 types 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err" |
15 types 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err" |
16 'a esl = "'a set * 'a ord * 'a ebinop" |
16 'a esl = "'a set * 'a ord * 'a ebinop" |