| changeset 972 | ebb4a40d9bae |
| parent 971 | 51e00f223792 |
| 971:51e00f223792 | 972:ebb4a40d9bae |
|---|---|
127 |
127 |
128 lemma Star_def2: |
128 lemma Star_def2: |
129 shows "A\<star> = (\<Union>n. A \<up> n)" |
129 shows "A\<star> = (\<Union>n. A \<up> n)" |
130 using Star_in_Pow Pow_in_Star |
130 using Star_in_Pow Pow_in_Star |
131 by (auto) |
131 by (auto) |
132 |
|
133 |
132 |
134 |
133 |
135 section \<open>Semantics of Regular Expressions\<close> |
134 section \<open>Semantics of Regular Expressions\<close> |
136 |
135 |
137 fun |
136 fun |