equal
deleted
inserted
replaced
107 shows "decode (code v) r = Some v" |
107 shows "decode (code v) r = Some v" |
108 using assms unfolding decode_def |
108 using assms unfolding decode_def |
109 by (smt append_Nil2 decode'_code old.prod.case) |
109 by (smt append_Nil2 decode'_code old.prod.case) |
110 |
110 |
111 |
111 |
112 section {* Annotated Regular Expressions *} |
112 section \<open>Annotated Regular Expressions\<close> |
113 |
113 |
114 datatype arexp = |
114 datatype arexp = |
115 AZERO |
115 AZERO |
116 | AONE "bit list" |
116 | AONE "bit list" |
117 | ACHAR "bit list" char |
117 | ACHAR "bit list" char |