thys/Journal/Paper.thy
changeset 288 9ab8609c66c5
parent 287 95b3880d428f
child 289 807acaf7f599
equal deleted inserted replaced
287:95b3880d428f 288:9ab8609c66c5
   297 %regular expressions than the initial one; various optimisations are
   297 %regular expressions than the initial one; various optimisations are
   298 %possible. We prove the correctness when simplifications of @{term "ALT ZERO r"}, 
   298 %possible. We prove the correctness when simplifications of @{term "ALT ZERO r"}, 
   299 %@{term "ALT r ZERO"}, @{term "SEQ ONE r"} and @{term "SEQ r ONE"} to
   299 %@{term "ALT r ZERO"}, @{term "SEQ ONE r"} and @{term "SEQ r ONE"} to
   300 %@{term r} are applied. 
   300 %@{term r} are applied. 
   301 
   301 
   302 We extend our results to ???
   302 We extend our results to ??? Bitcoded version??
   303 
   303 
   304 *}
   304 *}
   305 
   305 
   306 section {* Preliminaries *}
   306 section {* Preliminaries *}
   307 
   307