src/HOL/Corec_Examples/Stream_Processor.thy
changeset 62698 9d706e37ddab
parent 62694 f50d7efc8fe3
child 62726 5b2a7caa855b
     1.1 --- a/src/HOL/Corec_Examples/Stream_Processor.thy	Tue Mar 22 13:32:40 2016 +0100
     1.2 +++ b/src/HOL/Corec_Examples/Stream_Processor.thy	Tue Mar 22 13:44:50 2016 +0100
     1.3 @@ -66,7 +66,7 @@
     1.4    by (relation "map_prod In In ` sub <*lex*> map_prod In In ` sub")
     1.5      (auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image)
     1.6  
     1.7 -lemma run_copy_unique: 
     1.8 +lemma run_copy_unique:
     1.9      "(\<And>s. h s = shd s ## h (stl s)) \<Longrightarrow> h = run copy"
    1.10  apply corec_unique
    1.11  apply(rule ext)