author huffman Tue, 06 Sep 2011 16:30:39 -0700 changeset 44765 d96550db3d77 parent 44764 264436dd9491 (current diff) parent 44762 8f9d09241a68 (diff) child 44766 d4d33a4d7548
merged
```--- 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 @@

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 @@

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 @@

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```