src/HOL/HoareParallel/OG_Examples.thy
changeset 25112 98824cc791c0
parent 24075 366d4d234814
child 27095 c1c27955d7dd
     1.1 --- a/src/HOL/HoareParallel/OG_Examples.thy	Sat Oct 20 12:09:30 2007 +0200
     1.2 +++ b/src/HOL/HoareParallel/OG_Examples.thy	Sat Oct 20 12:09:33 2007 +0200
     1.3 @@ -439,7 +439,7 @@
     1.4  apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
     1.5  apply(simp_all (asm_lr) only:length_0_conv [THEN sym])
     1.6  --{* 44 subgoals left *}
     1.7 -apply (simp_all (asm_lr) del:length_0_conv add: nth_list_update mod_less_divisor mod_lemma)
     1.8 +apply (simp_all (asm_lr) del:length_0_conv add: neq0_conv nth_list_update mod_less_divisor mod_lemma)
     1.9  --{* 32 subgoals left *}
    1.10  apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
    1.11