--- 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
--- 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)) &