# HG changeset patch
# User wenzelm
# Date 1294846384 -3600
# Node ID 54b4686704af8bca09adecb51c0433e90b068858
# Parent  a42cbf5b44c82fe5941a6c92b6cacf3c0daa9d5e
eliminated global prems;

diff -r a42cbf5b44c8 -r 54b4686704af src/CCL/Set.thy
--- a/src/CCL/Set.thy	Wed Jan 12 15:53:37 2011 +0100
+++ b/src/CCL/Set.thy	Wed Jan 12 16:33:04 2011 +0100
@@ -222,7 +222,7 @@
 proof -
   have "\<not> (EX x. x:A) \<Longrightarrow> A = {}"
     by (rule equalityI) (blast intro!: subsetI elim!: emptyD)+
-  with prems show ?thesis by blast
+  with assms show ?thesis by blast
 qed
 
 
diff -r a42cbf5b44c8 -r 54b4686704af src/CCL/Type.thy
--- a/src/CCL/Type.thy	Wed Jan 12 15:53:37 2011 +0100
+++ b/src/CCL/Type.thy	Wed Jan 12 16:33:04 2011 +0100
@@ -214,7 +214,7 @@
 
 subsubsection {* Conversion Rules for Fixed Points via monotonicity and Tarski *}
 
-lemma NatM: "mono(%X. Unit+X)";
+lemma NatM: "mono(%X. Unit+X)"
   apply (rule PlusM constM idM)+
   done
 
@@ -358,7 +358,7 @@
   shows "t(a) : gfp(B)"
   apply (rule coinduct)
    apply (rule_tac P = "%x. EX y:A. x=t (y)" in CollectI)
-   apply (blast intro!: prems)+
+   apply (blast intro!: assms)+
   done
 
 lemma def_gfpI:
diff -r a42cbf5b44c8 -r 54b4686704af src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Wed Jan 12 15:53:37 2011 +0100
+++ b/src/CCL/Wfd.thy	Wed Jan 12 16:33:04 2011 +0100
@@ -253,11 +253,11 @@
   shows "letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"
   apply (unfold letrec2_def)
   apply (rule SPLITB [THEN subst])
-  apply (assumption | rule letrecT pairT splitT prems)+
+  apply (assumption | rule letrecT pairT splitT assms)+
   apply (subst SPLITB)
-  apply (assumption | rule ballI SubtypeI prems)+
+  apply (assumption | rule ballI SubtypeI assms)+
   apply (rule SPLITB [THEN subst])
-  apply (assumption | rule letrecT SubtypeI pairT splitT prems |
+  apply (assumption | rule letrecT SubtypeI pairT splitT assms |
     erule bspec SubtypeE sym [THEN subst])+
   done
 
@@ -275,11 +275,11 @@
   shows "letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"
   apply (unfold letrec3_def)
   apply (rule lem [THEN subst])
-  apply (assumption | rule letrecT pairT splitT prems)+
+  apply (assumption | rule letrecT pairT splitT assms)+
   apply (simp add: SPLITB)
-  apply (assumption | rule ballI SubtypeI prems)+
+  apply (assumption | rule ballI SubtypeI assms)+
   apply (rule lem [THEN subst])
-  apply (assumption | rule letrecT SubtypeI pairT splitT prems |
+  apply (assumption | rule letrecT SubtypeI pairT splitT assms |
     erule bspec SubtypeE sym [THEN subst])+
   done
 
@@ -520,7 +520,7 @@
   assumes "f ---> lam x. b(x)"
     and "b(a) ---> c"
   shows "f ` a ---> c"
-  unfolding apply_def by (eval prems)
+  unfolding apply_def by (eval assms)
 
 lemma letV:
   assumes 1: "t ---> a"
diff -r a42cbf5b44c8 -r 54b4686704af src/CCL/ex/Stream.thy
--- a/src/CCL/ex/Stream.thy	Wed Jan 12 15:53:37 2011 +0100
+++ b/src/CCL/ex/Stream.thy	Wed Jan 12 16:33:04 2011 +0100
@@ -63,7 +63,7 @@
   shows "map(f,l@m) = map(f,l) @ map(f,m)"
   apply (tactic {* eq_coinduct3_tac @{context}
     "{p. EX x y. p=<x,y> & (EX l:Lists (A). EX m:Lists (A). x=map (f,l@m) & y=map (f,l) @ map (f,m))}" 1 *})
-  apply (blast intro: prems)
+  apply (blast intro: assms)
   apply safe
   apply (drule ListsXH [THEN iffD1])
   apply (tactic "EQgen_tac @{context} [] 1")
@@ -82,7 +82,7 @@
   shows "k @ l @ m = (k @ l) @ m"
   apply (tactic {* eq_coinduct3_tac @{context}
     "{p. EX x y. p=<x,y> & (EX k:Lists (A). EX l:Lists (A). EX m:Lists (A). x=k @ l @ m & y= (k @ l) @ m) }" 1*})
-  apply (blast intro: prems)
+  apply (blast intro: assms)
   apply safe
   apply (drule ListsXH [THEN iffD1])
   apply (tactic "EQgen_tac @{context} [] 1")
@@ -100,7 +100,7 @@
   shows "l @ m = l"
   apply (tactic {* eq_coinduct3_tac @{context}
     "{p. EX x y. p=<x,y> & (EX l:ILists (A) .EX m. x=l@m & y=l)}" 1 *})
-  apply (blast intro: prems)
+  apply (blast intro: assms)
   apply safe
   apply (drule IListsXH [THEN iffD1])
   apply (tactic "EQgen_tac @{context} [] 1")
diff -r a42cbf5b44c8 -r 54b4686704af src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Wed Jan 12 15:53:37 2011 +0100
+++ b/src/CTT/CTT.thy	Wed Jan 12 16:33:04 2011 +0100
@@ -319,7 +319,7 @@
     and "a: A"
     and "!!z. z: B(a) ==> c(z): C(z)"
   shows "c(p`a): C(p`a)"
-apply (rule prems ProdE)+
+apply (rule assms ProdE)+
 done
 
 
diff -r a42cbf5b44c8 -r 54b4686704af src/CTT/ex/Elimination.thy
--- a/src/CTT/ex/Elimination.thy	Wed Jan 12 15:53:37 2011 +0100
+++ b/src/CTT/ex/Elimination.thy	Wed Jan 12 16:33:04 2011 +0100
@@ -145,7 +145,7 @@
 apply (rule subst_eqtyparg)
 apply (rule comp_rls)
 apply (rule_tac [4] SumE_snd)
-apply (tactic {* typechk_tac (@{thm SumE_fst} :: @{thms prems}) *})
+apply (tactic {* typechk_tac (@{thm SumE_fst} :: @{thms assms}) *})
 done
 
 text "Axiom of choice.  Proof without fst, snd.  Harder still!"
diff -r a42cbf5b44c8 -r 54b4686704af src/Cube/Cube.thy
--- a/src/Cube/Cube.thy	Wed Jan 12 15:53:37 2011 +0100
+++ b/src/Cube/Cube.thy	Wed Jan 12 16:33:04 2011 +0100
@@ -76,11 +76,11 @@
 
 lemma imp_elim:
   assumes "f:A->B" and "a:A" and "f^a:B ==> PROP P"
-  shows "PROP P" by (rule app prems)+
+  shows "PROP P" by (rule app assms)+
 
 lemma pi_elim:
   assumes "F:Prod(A,B)" and "a:A" and "F^a:B(a) ==> PROP P"
-  shows "PROP P" by (rule app prems)+
+  shows "PROP P" by (rule app assms)+
 
 
 locale L2 =
diff -r a42cbf5b44c8 -r 54b4686704af src/FOL/ex/Intro.thy
--- a/src/FOL/ex/Intro.thy	Wed Jan 12 15:53:37 2011 +0100
+++ b/src/FOL/ex/Intro.thy	Wed Jan 12 16:33:04 2011 +0100
@@ -76,7 +76,7 @@
   shows "~ P"
 apply (unfold not_def)
 apply (rule impI)
-apply (rule prems)
+apply (rule assms)
 apply assumption
 done
 
diff -r a42cbf5b44c8 -r 54b4686704af src/FOLP/ex/Foundation.thy
--- a/src/FOLP/ex/Foundation.thy	Wed Jan 12 15:53:37 2011 +0100
+++ b/src/FOLP/ex/Foundation.thy	Wed Jan 12 16:33:04 2011 +0100
@@ -23,17 +23,17 @@
   assumes "p : A & B"
     and "!!x y. x : A ==> y : B ==> f(x, y) : C"
   shows "?p : 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
 
 schematic_lemma
   assumes "!!A x. x : ~ ~A ==> cla(x) : A"
   shows "?p : B | ~B"
-apply (rule prems)
+apply (rule assms)
 apply (rule notI)
 apply (rule_tac P = "~B" in notE)
 apply (rule_tac [2] notI)
@@ -51,7 +51,7 @@
 schematic_lemma
   assumes "!!A x. x : ~ ~A ==> cla(x) : A"
   shows "?p : B | ~B"
-apply (rule prems)
+apply (rule assms)
 apply (rule notI)
 apply (rule notE)
 apply (rule_tac [2] notI)
@@ -68,11 +68,11 @@
     and "q : ~ ~A"
   shows "?p : 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
 
@@ -84,7 +84,7 @@
   shows "?p : ALL z. G(z)|H(z)"
 apply (rule allI)
 apply (rule disjI1)
-apply (rule prems [THEN spec])
+apply (rule assms [THEN spec])
 done
 
 schematic_lemma "?p : ALL x. EX y. x=y"
@@ -112,7 +112,7 @@
   assumes "p : (EX z. F(z)) & B"
   shows "?p : EX z. F(z) & B"
 apply (rule conjE)
-apply (rule prems)
+apply (rule assms)
 apply (rule exE)
 apply assumption
 apply (rule exI)
diff -r a42cbf5b44c8 -r 54b4686704af src/FOLP/ex/Intro.thy
--- 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
 
diff -r a42cbf5b44c8 -r 54b4686704af src/ZF/Induct/Tree_Forest.thy
--- a/src/ZF/Induct/Tree_Forest.thy	Wed Jan 12 15:53:37 2011 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy	Wed Jan 12 16:33:04 2011 +0100
@@ -176,7 +176,7 @@
   assumes "!!x. x \<in> A ==> h(x): B"
   shows map_tree_type: "t \<in> tree(A) ==> map(h,t) \<in> tree(B)"
     and map_forest_type: "f \<in> forest(A) ==> map(h,f) \<in> forest(B)"
-  using prems
+  using assms
   by (induct rule: tree'induct forest'induct) simp_all
 
 text {*