src/HOL/Algebra/Lattice.thy
changeset 15328 35951e6a7855
parent 14751 0d7850e27fed
child 16325 a6431098a929
--- 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