--- a/src/FOL/ex/Foundation.thy Wed Apr 16 11:24:09 2008 +0200
+++ b/src/FOL/ex/Foundation.thy Wed Apr 16 17:40:38 2008 +0200
@@ -24,17 +24,17 @@
assumes "A & B"
and "A ==> B ==> C"
shows C
-apply (rule prems)
+apply (rule assms)
apply (rule conjunct1)
-apply (rule prems)
+apply (rule assms)
apply (rule conjunct2)
-apply (rule prems)
+apply (rule assms)
done
lemma
assumes "!!A. ~ ~A ==> A"
shows "B | ~B"
-apply (rule prems)
+apply (rule assms)
apply (rule notI)
apply (rule_tac P = "~B" in notE)
apply (rule_tac [2] notI)
@@ -52,7 +52,7 @@
lemma
assumes "!!A. ~ ~A ==> A"
shows "B | ~B"
-apply (rule prems)
+apply (rule assms)
apply (rule notI)
apply (rule notE)
apply (rule_tac [2] notI)
@@ -69,11 +69,11 @@
and "~ ~A"
shows A
apply (rule disjE)
-apply (rule prems)
+apply (rule assms)
apply assumption
apply (rule FalseE)
apply (rule_tac P = "~A" in notE)
-apply (rule prems)
+apply (rule assms)
apply assumption
done
@@ -85,7 +85,7 @@
shows "ALL z. G(z)|H(z)"
apply (rule allI)
apply (rule disjI1)
-apply (rule prems [THEN spec])
+apply (rule assms [THEN spec])
done
lemma "ALL x. EX y. x=y"
@@ -113,7 +113,7 @@
assumes "(EX z. F(z)) & B"
shows "EX z. F(z) & B"
apply (rule conjE)
-apply (rule prems)
+apply (rule assms)
apply (rule exE)
apply assumption
apply (rule exI)