equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "../Closures" |
3 imports "../Closures" "../Attic/Prefix_subtract" |
4 begin |
4 begin |
5 |
5 |
6 declare [[show_question_marks = false]] |
6 declare [[show_question_marks = false]] |
7 |
7 |
8 consts |
8 consts |
1288 \end{tabular} |
1288 \end{tabular} |
1289 \end{center} |
1289 \end{center} |
1290 % |
1290 % |
1291 \noindent |
1291 \noindent |
1292 and \emph{string subtraction}: |
1292 and \emph{string subtraction}: |
1293 % |
1293 |
1294 \begin{center} |
|
1295 \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
|
1296 @{text "[] - y"} & @{text "\<equiv>"} & @{text "[]"}\\ |
|
1297 @{text "x - []"} & @{text "\<equiv>"} & @{text "x"}\\ |
|
1298 @{text "cx - dy"} & @{text "\<equiv>"} & @{text "if c = d then x - y else cx"} |
|
1299 \end{tabular} |
|
1300 \end{center} |
|
1301 % |
|
1302 \noindent |
1294 \noindent |
1303 where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings. |
1295 where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings. |
1304 |
1296 |
1305 Now assuming @{term "x @ z \<in> A \<cdot> B"} there are only two possible ways of how to `split' |
1297 Now assuming @{term "x @ z \<in> A \<cdot> B"} there are only two possible ways of how to `split' |
1306 this string to be in @{term "A \<cdot> B"}: |
1298 this string to be in @{term "A \<cdot> B"}: |