changeset 20503 | 503ac4c5ef91 |
parent 19736 | d8d0f8f51d69 |
child 21404 | eb85850d3eb7 |
--- a/src/HOL/Induct/PropLog.thy Mon Sep 11 14:35:30 2006 +0200 +++ b/src/HOL/Induct/PropLog.thy Mon Sep 11 21:35:19 2006 +0200 @@ -259,7 +259,7 @@ by (unfold sat_def, auto) theorem completeness: "finite H ==> H |= p ==> H |- p" -apply (induct fixing: p rule: finite_induct) +apply (induct arbitrary: p rule: finite_induct) apply (blast intro: completeness_0) apply (iprover intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP]) done