equal
deleted
inserted
replaced
1154 apply(induct r rule: bsimp.induct) |
1154 apply(induct r rule: bsimp.induct) |
1155 apply(auto) |
1155 apply(auto) |
1156 using bsimp_ASEQ_idem apply presburger |
1156 using bsimp_ASEQ_idem apply presburger |
1157 oops |
1157 oops |
1158 |
1158 |
|
1159 |
|
1160 lemma normal_form: |
|
1161 shows "\<forall>r. \<nexists> r'. bsimp r \<leadsto> r'" |
|
1162 |
|
1163 oops |
|
1164 |
|
1165 lemma another_normal: |
|
1166 shows "\<nexists>r'. bsimp r \<leadsto> r'" |
|
1167 oops |
|
1168 |
1159 export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers |
1169 export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers |
1160 |
1170 |
1161 |
1171 |
1162 unused_thms |
1172 unused_thms |
1163 |
1173 |