# HG changeset patch
# User wenzelm
# Date 1294849190 -3600
# Node ID ba60efa2fd08a1972e4657147869f4f6e2f446b3
# Parent  276078f01ada4db73a0902a8b3a4b5b6251c628a
eliminated global prems;

diff -r 276078f01ada -r ba60efa2fd08 src/HOL/Bali/AxSound.thy
--- a/src/HOL/Bali/AxSound.thy	Wed Jan 12 17:14:27 2011 +0100
+++ b/src/HOL/Bali/AxSound.thy	Wed Jan 12 17:19:50 2011 +0100
@@ -293,7 +293,7 @@
    and    da: "normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>C"
    and    elim: "\<lbrakk>Q v s1 Z; s1\<Colon>\<preceq>(G,L)\<rbrakk> \<Longrightarrow> concl" 
   shows concl
-using prems
+using assms
 by (simp add: ax_valids2_def triple_valid2_def2) fast
 (* why consumes 5?. If I want to apply this lemma in a context wgere
    \<not> normal s0 holds,
diff -r 276078f01ada -r ba60efa2fd08 src/HOL/HOLCF/Completion.thy
--- a/src/HOL/HOLCF/Completion.thy	Wed Jan 12 17:14:27 2011 +0100
+++ b/src/HOL/HOLCF/Completion.thy	Wed Jan 12 17:19:50 2011 +0100
@@ -26,7 +26,7 @@
   assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. x \<preceq> z \<and> y \<preceq> z"
   assumes "\<And>x y. \<lbrakk>x \<preceq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
   shows "ideal A"
-unfolding ideal_def using prems by fast
+unfolding ideal_def using assms by fast
 
 lemma idealD1:
   "ideal A \<Longrightarrow> \<exists>x. x \<in> A"
diff -r 276078f01ada -r ba60efa2fd08 src/HOL/HOLCF/Domain.thy
--- a/src/HOL/HOLCF/Domain.thy	Wed Jan 12 17:14:27 2011 +0100
+++ b/src/HOL/HOLCF/Domain.thy	Wed Jan 12 17:19:50 2011 +0100
@@ -211,7 +211,7 @@
   assumes "chain d" and "chain t"
   assumes "\<And>i. isodefl (d i) (t i)"
   shows "isodefl (\<Squnion>i. d i) (\<Squnion>i. t i)"
-using prems unfolding isodefl_def
+using assms unfolding isodefl_def
 by (simp add: contlub_cfun_arg contlub_cfun_fun)
 
 lemma isodefl_fix:
diff -r 276078f01ada -r ba60efa2fd08 src/HOL/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Wed Jan 12 17:14:27 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Wed Jan 12 17:19:50 2011 +0100
@@ -312,7 +312,7 @@
 apply (intro strip)
 apply (erule exE)
 apply (erule subst)
-apply (rule prems)
+apply (rule assms)
 done
 
 
diff -r 276078f01ada -r ba60efa2fd08 src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Wed Jan 12 17:14:27 2011 +0100
+++ b/src/HOL/HOLCF/Universal.thy	Wed Jan 12 17:19:50 2011 +0100
@@ -183,7 +183,7 @@
   case (ubasis_le_upper S b a i) thus ?case
     apply clarsimp
     apply (subst ubasis_until_same)
-     apply (erule (3) prems)
+     apply (erule (3) assms)
     apply (erule (2) ubasis_le.ubasis_le_upper)
     done
 qed
diff -r 276078f01ada -r ba60efa2fd08 src/HOL/IMP/Natural.thy
--- a/src/HOL/IMP/Natural.thy	Wed Jan 12 17:14:27 2011 +0100
+++ b/src/HOL/IMP/Natural.thy	Wed Jan 12 17:19:50 2011 +0100
@@ -1,5 +1,4 @@
 (*  Title:        HOL/IMP/Natural.thy
-    ID:           $Id$
     Author:       Tobias Nipkow & Robert Sandner, TUM
     Isar Version: Gerwin Klein, 2001; additional proofs by Lawrence Paulson
     Copyright     1996 TUM
@@ -270,7 +269,7 @@
 theorem com_det:
   assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
   shows "u = t"
-  using prems
+  using assms
 proof (induct arbitrary: u set: evalc)
   fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
   thus "u = s" by blast
@@ -331,7 +330,7 @@
 theorem
   assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
   shows "u = t"
-  using prems
+  using assms
 proof (induct arbitrary: u)
   -- "the simple @{text \<SKIP>} case for demonstration:"
   fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
diff -r 276078f01ada -r ba60efa2fd08 src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Transition.thy	Wed Jan 12 17:14:27 2011 +0100
+++ b/src/HOL/IMP/Transition.thy	Wed Jan 12 17:19:50 2011 +0100
@@ -272,7 +272,7 @@
 lemma evalc_imp_evalc1:
   assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
   shows "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-  using prems
+  using assms
 proof induct
   fix s show "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" by auto
 next
@@ -550,7 +550,7 @@
   shows "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
 proof -
   -- {* The induction rule needs @{text P} to be a function of @{term "Some c1"} *}
-  from prems
+  from assms
   have "\<langle>(\<lambda>c. if c = None then c2 else the c; c2) (Some c1),s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
     apply (induct rule: converse_rtrancl_induct2)
      apply simp
diff -r 276078f01ada -r ba60efa2fd08 src/HOL/IMPP/Hoare.thy
--- a/src/HOL/IMPP/Hoare.thy	Wed Jan 12 17:14:27 2011 +0100
+++ b/src/HOL/IMPP/Hoare.thy	Wed Jan 12 17:19:50 2011 +0100
@@ -369,18 +369,18 @@
 prefer 2
 apply   (simp add: card_seteq)
 apply  simp
-apply  (erule prems(3-)) (*MGF_lemma1*)
+apply  (erule assms(3-)) (*MGF_lemma1*)
 apply (rule ballI)
-apply  (rule prems) (*hoare_derivs.asm*)
+apply  (rule assms) (*hoare_derivs.asm*)
 apply  fast
-apply (erule prems(3-)) (*MGF_lemma1*)
+apply (erule assms(3-)) (*MGF_lemma1*)
 apply (rule ballI)
 apply (case_tac "mgt_call pn : G")
-apply  (rule prems) (*hoare_derivs.asm*)
+apply  (rule assms) (*hoare_derivs.asm*)
 apply  fast
-apply (rule prems(2-)) (*MGT_BodyN*)
+apply (rule assms(2-)) (*MGT_BodyN*)
 apply (drule spec, erule impE, erule_tac [2] impE, drule_tac [3] spec, erule_tac [3] mp)
-apply   (erule_tac [3] prems(4-))
+apply   (erule_tac [3] assms(4-))
 apply   fast
 apply (drule finite_subset)
 apply (erule finite_imageI)
diff -r 276078f01ada -r ba60efa2fd08 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Jan 12 17:14:27 2011 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Jan 12 17:19:50 2011 +0100
@@ -793,7 +793,7 @@
   assumes "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
   and "degree p = n" and "n \<noteq> 0"
   shows "p dvd (q ^ n)"
-using prems
+using assms
 proof(induct n arbitrary: p q rule: nat_less_induct)
   fix n::nat fix p q :: "complex poly"
   assume IH: "\<forall>m<n. \<forall>p q.
diff -r 276078f01ada -r ba60efa2fd08 src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Wed Jan 12 17:14:27 2011 +0100
+++ b/src/HOL/TLA/TLA.thy	Wed Jan 12 17:19:50 2011 +0100
@@ -520,7 +520,7 @@
   shows "|- []P --> []A"
   apply clarsimp
   apply (drule BoxPrime [temp_use])
-  apply (auto simp: Init_stp_act_rev [try_rewrite] intro!: prems [temp_use]
+  apply (auto simp: Init_stp_act_rev [try_rewrite] intro!: assms [temp_use]
     elim!: STL4E [temp_use])
   done