# HG changeset patch
# User nipkow
# Date 1101291180 -3600
# Node ID 35951e6a785533fca26cdf79a50b39a8564f792a
# Parent  0230a10582d3b64840ffa01595251ed5297353d5
mod because of change in finite set induction

diff -r 0230a10582d3 -r 35951e6a7855 src/HOL/Algebra/CRing.thy
--- 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 *}
diff -r 0230a10582d3 -r 35951e6a7855 src/HOL/Algebra/FiniteProduct.thy
--- 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)
diff -r 0230a10582d3 -r 35951e6a7855 src/HOL/Algebra/Lattice.thy
--- 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