# HG changeset patch
# User haftmann
# Date 1248781028 -7200
# Node ID 8bc0fd4a23a087d4d4d844a6d3a3f1c7e5fa3466
# Parent  0c1cb95a434d8f1ca0dec5370d5cf3bf2f37b2f8
explicit is better than implicit

diff -r 0c1cb95a434d -r 8bc0fd4a23a0 src/HOL/MicroJava/BV/Listn.thy
--- a/src/HOL/MicroJava/BV/Listn.thy	Tue Jul 28 08:49:03 2009 +0200
+++ b/src/HOL/MicroJava/BV/Listn.thy	Tue Jul 28 13:37:08 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/BV/Listn.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   2000 TUM
 
@@ -8,7 +7,9 @@
 
 header {* \isaheader{Fixed Length Lists} *}
 
-theory Listn imports Err begin
+theory Listn
+imports Err
+begin
 
 constdefs
 
@@ -317,6 +318,10 @@
 apply (simp add: nth_Cons split: nat.split)
 done
 
+lemma equals0I_aux:
+  "(\<And>y. A y \<Longrightarrow> False) \<Longrightarrow> A = bot_class.bot"
+  by (rule equals0I) (auto simp add: mem_def)
+
 lemma acc_le_listI [intro!]:
   "\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
 apply (unfold acc_def)
@@ -330,7 +335,7 @@
  apply (rename_tac m n)
  apply (case_tac "m=n")
   apply simp
- apply (fast intro!: equals0I [to_pred bot_empty_eq pred_equals_eq] dest: not_sym)
+ apply (fast intro!: equals0I_aux dest: not_sym)
 apply clarify
 apply (rename_tac n)
 apply (induct_tac n)
diff -r 0c1cb95a434d -r 8bc0fd4a23a0 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Jul 28 08:49:03 2009 +0200
+++ b/src/HOL/Wellfounded.thy	Tue Jul 28 13:37:08 2009 +0200
@@ -283,8 +283,10 @@
 apply (blast elim!: allE)  
 done
 
-lemmas wfP_SUP = wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}",
-  to_pred SUP_UN_eq2 bot_empty_eq pred_equals_eq, simplified, standard]
+lemma wfP_SUP:
+  "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPR UNIV r)"
+  by (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2 pred_equals_eq])
+    (simp_all add: bot_fun_eq bot_bool_eq)
 
 lemma wf_Union: 
  "[| ALL r:R. wf r;