author huffman Tue Sep 06 16:30:39 2011 -0700 (2011-09-06) changeset 44765 d96550db3d77 parent 44764 264436dd9491 parent 44762 8f9d09241a68 child 44766 d4d33a4d7548
merged
```     1.1 --- a/src/HOL/Statespace/StateFun.thy	Tue Sep 06 14:53:51 2011 -0700
1.2 +++ b/src/HOL/Statespace/StateFun.thy	Tue Sep 06 16:30:39 2011 -0700
1.3 @@ -28,7 +28,7 @@
1.5
1.6  lemma K_statefun_comp [simp]: "(K_statefun c \<circ> f) = K_statefun c"
1.7 -  by (rule ext) (simp add: K_statefun_apply comp_def)
1.8 +  by (rule ext) (simp add: comp_def)
1.9
1.10  lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
1.11    by (rule refl)
```
```     2.1 --- a/src/HOL/Word/Examples/WordExamples.thy	Tue Sep 06 14:53:51 2011 -0700
2.2 +++ b/src/HOL/Word/Examples/WordExamples.thy	Tue Sep 06 16:30:39 2011 -0700
2.3 @@ -7,7 +7,7 @@
2.4  header "Examples of word operations"
2.5
2.6  theory WordExamples
2.7 -imports Word
2.8 +imports "../Word"
2.9  begin
2.10
2.11  type_synonym word32 = "32 word"
```
```     3.1 --- a/src/HOL/Word/Word.thy	Tue Sep 06 14:53:51 2011 -0700
3.2 +++ b/src/HOL/Word/Word.thy	Tue Sep 06 16:30:39 2011 -0700
3.3 @@ -455,12 +455,12 @@
3.4    by (simp add: number_of_eq word_number_of_def)
3.5
3.6  lemma word_no_wi: "number_of = word_of_int"
3.7 -  by (auto simp: word_number_of_def intro: ext)
3.8 +  by (auto simp: word_number_of_def)
3.9
3.10  lemma to_bl_def':
3.11    "(to_bl :: 'a :: len0 word => bool list) =
3.12      bin_to_bl (len_of TYPE('a)) o uint"
3.13 -  by (auto simp: to_bl_def intro: ext)
3.14 +  by (auto simp: to_bl_def)
3.15
3.16  lemmas word_reverse_no_def [simp] = word_reverse_def [of "number_of w", standard]
3.17
3.18 @@ -4230,8 +4230,6 @@
3.19
3.20  (* using locale to not pollute lemma namespace *)
3.21  locale word_rotate
3.22 -
3.23 -context word_rotate
3.24  begin
3.25
3.26  lemmas word_rot_defs' = to_bl_rotl to_bl_rotr
```