equal
deleted
inserted
replaced
7 |
7 |
8 theory Err |
8 theory Err |
9 imports Semilat |
9 imports Semilat |
10 begin |
10 begin |
11 |
11 |
12 datatype 'a err = Err | OK 'a |
12 datatype_new 'a err = Err | OK 'a |
13 |
13 |
14 type_synonym 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err" |
14 type_synonym 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err" |
15 type_synonym 'a esl = "'a set * 'a ord * 'a ebinop" |
15 type_synonym 'a esl = "'a set * 'a ord * 'a ebinop" |
16 |
16 |
17 primrec ok_val :: "'a err \<Rightarrow> 'a" where |
17 primrec ok_val :: "'a err \<Rightarrow> 'a" where |