equal
deleted
inserted
replaced
509 apply(simp_all add:mul_modules) |
509 apply(simp_all add:mul_modules) |
510 apply(simp_all add:mul_collector_defs Queue_def) |
510 apply(simp_all add:mul_collector_defs Queue_def) |
511 apply force |
511 apply force |
512 apply force |
512 apply force |
513 apply force |
513 apply force |
514 apply (force simp add: less_Suc_eq_le length_filter) |
514 apply (force simp add: less_Suc_eq_le) |
515 apply force |
515 apply force |
516 apply (force dest:subset_antisym) |
516 apply (force dest:subset_antisym) |
517 apply force |
517 apply force |
518 apply force |
518 apply force |
519 apply force |
519 apply force |