# HG changeset patch
# User nipkow
# Date 1178909250 -7200
# Node ID 314b45eb422d5cea183cb3af337bbe89702f483d
# Parent  42de50e78446109c3740c1389764ab96a7149f52
*** empty log message ***

diff -r 42de50e78446 -r 314b45eb422d src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri May 11 20:07:00 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Fri May 11 20:47:30 2007 +0200
@@ -2397,20 +2397,14 @@
 *}
 
 lemma (in complete_lattice) Inf_fold1:
-  assumes fin: "finite A"
-  and nonempty: "A \<noteq> {}"
-  shows "\<Sqinter>A = fold1 (op \<sqinter>) A"
-using fin nonempty 
+  "finite A \<Longrightarrow>  A \<noteq> {} \<Longrightarrow> \<Sqinter>A = fold1 (op \<sqinter>) A"
 by (induct A set: finite)
-  (simp_all add: Inf_insert_simp ACIf.fold1_insert_idem [OF ACIf_inf])
+   (simp_all add: Inf_insert_simp ACIf.fold1_insert_idem [OF ACIf_inf])
 
 lemma (in complete_lattice) Sup_fold1:
-  assumes fin: "finite A"
-  and nonempty: "A \<noteq> {}"
-  shows "\<Squnion>A = fold1 (op \<squnion>) A"
-using fin nonempty 
+"finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Squnion>A = fold1 (op \<squnion>) A"
 by (induct A set: finite)
-  (simp_all add: Sup_insert_simp ACIf.fold1_insert_idem [OF ACIf_sup])
+   (simp_all add: Sup_insert_simp ACIf.fold1_insert_idem [OF ACIf_sup])
 
 
 subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}