| changeset 37456 | 0a1cc2675958 |
| parent 36147 | b43b22f63665 |
| child 37709 | 70fafefbcc98 |
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Fri Jun 18 14:14:42 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Fri Jun 18 20:22:06 2010 +0200 @@ -555,7 +555,6 @@ apply auto apply (drule fold_steps_correct) apply (simp add: correctArray_def array_ran_def) -apply (cases "n = 0", auto) apply (rule implies_empty_inconsistent) apply (simp add:correctArray_def) apply (drule bspec)