# HG changeset patch
# User haftmann
# Date 1277731945 -7200
# Node ID 1840dc0265da89461a605b40e8f51821a4a9cf69
# Parent  6e89e103f7c7091c3f005b96cad2f72c916587fc
explicit is better than implicit

diff -r 6e89e103f7c7 -r 1840dc0265da src/HOL/NanoJava/Equivalence.thy
--- a/src/HOL/NanoJava/Equivalence.thy	Mon Jun 28 15:32:25 2010 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy	Mon Jun 28 15:32:25 2010 +0200
@@ -133,7 +133,7 @@
  apply  (clarify intro!: Impl_nvalid_0)
 apply (clarify  intro!: Impl_nvalid_Suc)
 apply (drule nvalids_SucD)
-apply (simp only: all_simps)
+apply (simp only: HOL.all_simps)
 apply (erule (1) impE)
 apply (drule (2) Impl_sound_lemma)
  apply  blast
diff -r 6e89e103f7c7 -r 1840dc0265da src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Mon Jun 28 15:32:25 2010 +0200
+++ b/src/HOL/Word/WordShift.thy	Mon Jun 28 15:32:25 2010 +0200
@@ -988,8 +988,10 @@
    apply (erule bin_nth_uint_imp)+
   done
 
-lemmas test_bit_split = 
-  test_bit_split' [THEN mp, simplified all_simps, standard]
+lemma test_bit_split:
+  "word_split c = (a, b) \<Longrightarrow>
+    (\<forall>n\<Colon>nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and> (\<forall>m\<Colon>nat. a !! m \<longleftrightarrow> m < size a \<and> c !! (m + size b))"
+  by (simp add: test_bit_split')
 
 lemma test_bit_split_eq: "word_split c = (a, b) <-> 
   ((ALL n::nat. b !! n = (n < size b & c !! n)) &