--- a/src/HOL/Algebra/CRing.thy Wed Nov 24 11:12:10 2004 +0100
+++ b/src/HOL/Algebra/CRing.thy Wed Nov 24 11:13:00 2004 +0100
@@ -476,7 +476,7 @@
proof (induct set: Finites)
case empty then show ?case by simp
next
- case (insert F x) then show ?case by (simp add: Pi_def l_distr)
+ case (insert x F) then show ?case by (simp add: Pi_def l_distr)
qed
lemma (in cring) finsum_rdistr:
@@ -485,7 +485,7 @@
proof (induct set: Finites)
case empty then show ?case by simp
next
- case (insert F x) then show ?case by (simp add: Pi_def r_distr)
+ case (insert x F) then show ?case by (simp add: Pi_def r_distr)
qed
subsection {* Facts of Integral Domains *}
--- a/src/HOL/Algebra/FiniteProduct.thy Wed Nov 24 11:12:10 2004 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy Wed Nov 24 11:13:00 2004 +0100
@@ -50,7 +50,7 @@
proof (induct set: Finites)
case empty then show ?case by auto
next
- case (insert F x)
+ case (insert x F)
then obtain y where y: "(F, y) \<in> foldSetD D f e" by auto
with insert have "y \<in> D" by (auto dest: foldSetD_closed)
with y and insert have "(insert x F, f x y) \<in> foldSetD D f e"
@@ -90,7 +90,7 @@
proof (induct set: Finites)
case empty then show ?case by auto
next
- case (insert F x)
+ case (insert x F)
then obtain y where y: "(F, y) \<in> foldSetD D f e" by auto
with insert have "y \<in> D" by auto
with y and insert have "(insert x F, f x y) \<in> foldSetD D f e"
@@ -339,7 +339,7 @@
proof (induct set: Finites)
case empty show ?case by simp
next
- case (insert A a)
+ case (insert a A)
have "(%i. \<one>) \<in> A -> carrier G" by auto
with insert show ?case by simp
qed
@@ -352,7 +352,7 @@
proof induct
case empty show ?case by simp
next
- case (insert A a)
+ case (insert a A)
then have a: "f a \<in> carrier G" by fast
from insert have A: "f \<in> A -> carrier G" by fast
from insert A a show ?case by simp
@@ -374,7 +374,7 @@
proof (induct set: Finites)
case empty then show ?case by (simp add: finprod_closed)
next
- case (insert A a)
+ case (insert a A)
then have a: "g a \<in> carrier G" by fast
from insert have A: "g \<in> A -> carrier G" by fast
from insert A a show ?case
@@ -396,7 +396,7 @@
proof (induct set: Finites)
case empty show ?case by simp
next
- case (insert A a) then
+ case (insert a A) then
have fA: "f \<in> A -> carrier G" by fast
from insert have fa: "f a \<in> carrier G" by fast
from insert have gA: "g \<in> A -> carrier G" by fast
@@ -421,7 +421,7 @@
proof induct
case empty thus ?case by simp
next
- case (insert B x)
+ case (insert x B)
then have "finprod G f A = finprod G f (insert x B)" by simp
also from insert have "... = f x \<otimes> finprod G f B"
proof (intro finprod_insert)
--- a/src/HOL/Algebra/Lattice.thy Wed Nov 24 11:12:10 2004 +0100
+++ b/src/HOL/Algebra/Lattice.thy Wed Nov 24 11:13:00 2004 +0100
@@ -320,7 +320,7 @@
case empty
then show ?case by simp
next
- case (insert A x)
+ case (insert x A)
show ?case
proof (cases "A = {}")
case True
@@ -350,7 +350,7 @@
proof (induct set: Finites)
case empty then show ?case by simp
next
- case (insert A x) then show ?case
+ case insert then show ?case
by - (rule finite_sup_insertI, simp_all)
qed
@@ -546,7 +546,7 @@
proof (induct set: Finites)
case empty then show ?case by simp
next
- case (insert A x)
+ case (insert x A)
show ?case
proof (cases "A = {}")
case True
@@ -577,7 +577,7 @@
proof (induct set: Finites)
case empty then show ?case by simp
next
- case (insert A x) then show ?case
+ case insert then show ?case
by (rule_tac finite_inf_insertI) (simp_all)
qed