merged
authorhuffman
Tue Sep 06 16:30:39 2011 -0700 (2011-09-06)
changeset 44765d96550db3d77
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.4    by (simp add: K_statefun_def)
     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