equal
deleted
inserted
replaced
284 \begin{tabular}{lcl} |
284 \begin{tabular}{lcl} |
285 @{thm[mode=Rule] aggressive.intros(1)[of "bs" "bs1" "rs" "r"]}\\ |
285 @{thm[mode=Rule] aggressive.intros(1)[of "bs" "bs1" "rs" "r"]}\\ |
286 \end{tabular} |
286 \end{tabular} |
287 \end{center} |
287 \end{center} |
288 |
288 |
289 |
|
290 This rule allows us to simplify \mbox{@{term "ALT (SEQ (ALT a b) c) (SEQ a c)"}} |
289 This rule allows us to simplify \mbox{@{term "ALT (SEQ (ALT a b) c) (SEQ a c)"}} |
|
290 |
|
291 \<close> |
|
292 |
|
293 (*This rule allows us to simplify \mbox{@{term "ALT (SEQ (ALT a b) c) (SEQ a c)"}} |
291 into \mbox{@{term "ALT (SEQ a c) (SEQ b c)"}}, |
294 into \mbox{@{term "ALT (SEQ a c) (SEQ b c)"}}, |
292 which is cannot be done under the \<leadsto> rule because only alternatives which are |
295 which is cannot be done under the \<leadsto> rule because only alternatives which are |
293 children of another alternative can be spilled out. |
296 children of another alternative can be spilled out.*) |
294 \<close> |
|
295 |
|
296 |
|
297 section \<open>Introduction\<close> |
297 section \<open>Introduction\<close> |
298 |
298 |
299 |
299 |
300 text \<open> |
300 text \<open> |
301 |
301 |