# HG changeset patch
# User huffman
# Date 1315351839 25200
# Node ID d96550db3d77f7736532d62ea0876af58507b533
# Parent  264436dd949106a22d935fef05a06321d94ab255# Parent  8f9d09241a686e3a4180285545d5143c42ba0d54
merged

diff -r 264436dd9491 -r d96550db3d77 src/HOL/Statespace/StateFun.thy
--- a/src/HOL/Statespace/StateFun.thy	Tue Sep 06 14:53:51 2011 -0700
+++ b/src/HOL/Statespace/StateFun.thy	Tue Sep 06 16:30:39 2011 -0700
@@ -28,7 +28,7 @@
   by (simp add: K_statefun_def)
 
 lemma K_statefun_comp [simp]: "(K_statefun c \<circ> f) = K_statefun c"
-  by (rule ext) (simp add: K_statefun_apply comp_def)
+  by (rule ext) (simp add: comp_def)
 
 lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
   by (rule refl)
diff -r 264436dd9491 -r d96550db3d77 src/HOL/Word/Examples/WordExamples.thy
--- a/src/HOL/Word/Examples/WordExamples.thy	Tue Sep 06 14:53:51 2011 -0700
+++ b/src/HOL/Word/Examples/WordExamples.thy	Tue Sep 06 16:30:39 2011 -0700
@@ -7,7 +7,7 @@
 header "Examples of word operations"
 
 theory WordExamples
-imports Word
+imports "../Word"
 begin
 
 type_synonym word32 = "32 word"
diff -r 264436dd9491 -r d96550db3d77 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Sep 06 14:53:51 2011 -0700
+++ b/src/HOL/Word/Word.thy	Tue Sep 06 16:30:39 2011 -0700
@@ -455,12 +455,12 @@
   by (simp add: number_of_eq word_number_of_def)
 
 lemma word_no_wi: "number_of = word_of_int"
-  by (auto simp: word_number_of_def intro: ext)
+  by (auto simp: word_number_of_def)
 
 lemma to_bl_def': 
   "(to_bl :: 'a :: len0 word => bool list) =
     bin_to_bl (len_of TYPE('a)) o uint"
-  by (auto simp: to_bl_def intro: ext)
+  by (auto simp: to_bl_def)
 
 lemmas word_reverse_no_def [simp] = word_reverse_def [of "number_of w", standard]
 
@@ -4230,8 +4230,6 @@
 
 (* using locale to not pollute lemma namespace *)
 locale word_rotate 
-
-context word_rotate
 begin
 
 lemmas word_rot_defs' = to_bl_rotl to_bl_rotr