equal
deleted
inserted
replaced
441 --{* 44 subgoals left *} |
441 --{* 44 subgoals left *} |
442 apply (simp_all (asm_lr) del:length_0_conv add: nth_list_update mod_less_divisor mod_lemma) |
442 apply (simp_all (asm_lr) del:length_0_conv add: nth_list_update mod_less_divisor mod_lemma) |
443 --{* 32 subgoals left *} |
443 --{* 32 subgoals left *} |
444 apply(tactic {* ALLGOALS (clarify_tac @{claset}) *}) |
444 apply(tactic {* ALLGOALS (clarify_tac @{claset}) *}) |
445 |
445 |
446 apply(tactic {* TRYALL simple_arith_tac *}) |
446 apply(tactic {* TRYALL (simple_arith_tac @{context}) *}) |
447 --{* 9 subgoals left *} |
447 --{* 9 subgoals left *} |
448 apply (force simp add:less_Suc_eq) |
448 apply (force simp add:less_Suc_eq) |
449 apply(drule sym) |
449 apply(drule sym) |
450 apply (force simp add:less_Suc_eq)+ |
450 apply (force simp add:less_Suc_eq)+ |
451 done |
451 done |