--- a/src/FOL/ex/Intro.thy Wed Jan 12 15:53:37 2011 +0100 +++ b/src/FOL/ex/Intro.thy Wed Jan 12 16:33:04 2011 +0100 @@ -76,7 +76,7 @@ shows "~ P" apply (unfold not_def) apply (rule impI) -apply (rule prems) +apply (rule assms) apply assumption done