| changeset 971 | b7d97a2a083b |
| parent 970 | e15be5466802 |
| child 1009 | 7fd1997bd14c |
| 970:e15be5466802 | 971:b7d97a2a083b |
|---|---|
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 |