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