--- 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
--- 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:
--- 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"
--- 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")
--- 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
--- 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!"
--- 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 =
--- 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
--- 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)
--- 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
--- 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 {*