# HG changeset patch
# User wenzelm
# Date 1208360438 -7200
# Node ID 310c3b1a4157e65e577f97606544c8d8770a67dc
# Parent  19e1d3c96f2f2b30406612e0001bb938e0fbc9cd
tuned proofs;

diff -r 19e1d3c96f2f -r 310c3b1a4157 src/FOL/ex/Foundation.thy
--- 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)