--- 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,
--- 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"
--- 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:
--- 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
--- 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
--- 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"
--- 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
--- 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)
--- 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.
--- 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