src/FOLP/ex/Intro.thy
changeset 41526 54b4686704af
parent 36319 8feb2c4bef1a
child 58889 5b7a9633cfa8
--- a/src/FOLP/ex/Intro.thy	Wed Jan 12 15:53:37 2011 +0100
+++ b/src/FOLP/ex/Intro.thy	Wed Jan 12 16:33:04 2011 +0100
@@ -76,7 +76,7 @@
   shows "?p : ~ P"
 apply (unfold not_def)
 apply (rule impI)
-apply (rule prems)
+apply (rule assms)
 apply assumption
 done