# HG changeset patch
# User wenzelm
# Date 1315346889 -7200
# Node ID 8f9d09241a686e3a4180285545d5143c42ba0d54
# Parent  0694fc3248fdec2aabaa18589d3b8f0aff1716aa
tuned proofs;

diff -r 0694fc3248fd -r 8f9d09241a68 src/HOL/Statespace/StateFun.thy
--- a/src/HOL/Statespace/StateFun.thy	Tue Sep 06 13:16:46 2011 -0700
+++ b/src/HOL/Statespace/StateFun.thy	Wed Sep 07 00:08:09 2011 +0200
@@ -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 0694fc3248fd -r 8f9d09241a68 src/HOL/Word/Examples/WordExamples.thy
--- a/src/HOL/Word/Examples/WordExamples.thy	Tue Sep 06 13:16:46 2011 -0700
+++ b/src/HOL/Word/Examples/WordExamples.thy	Wed Sep 07 00:08:09 2011 +0200
@@ -7,7 +7,7 @@
 header "Examples of word operations"
 
 theory WordExamples
-imports Word
+imports "../Word"
 begin
 
 type_synonym word32 = "32 word"
diff -r 0694fc3248fd -r 8f9d09241a68 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Sep 06 13:16:46 2011 -0700
+++ b/src/HOL/Word/Word.thy	Wed Sep 07 00:08:09 2011 +0200
@@ -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