| changeset 102 | 5fed809d0fc1 |
| parent 24 | f72c82bf59e5 |
| child 103 | f460d5f75cb5 |
| 101:d3fe0597080a | 102:5fed809d0fc1 |
|---|---|
34 | EMPTY |
34 | EMPTY |
35 | CHAR char |
35 | CHAR char |
36 | SEQ rexp rexp |
36 | SEQ rexp rexp |
37 | ALT rexp rexp |
37 | ALT rexp rexp |
38 | STAR rexp |
38 | STAR rexp |
39 |
|
40 |
|
41 definition |
|
42 "DERIV s A \<equiv> {s'. s @ s' \<in> A}" |
|
43 |
|
44 definition |
|
45 "delta A = (if [] \<in> A then {[]} else {})" |
|
46 |
|
39 |
47 |
40 |
48 |
41 section {* Semantics of Regular Expressions *} |
49 section {* Semantics of Regular Expressions *} |
42 |
50 |
43 fun |
51 fun |