src/HOL/BNF_Examples/Stream.thy
changeset 57983 6edc3529bb4e
parent 57206 d9be905d6283
child 57986 0d60b9e58487
     1.1 --- a/src/HOL/BNF_Examples/Stream.thy	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/BNF_Examples/Stream.thy	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -49,9 +49,9 @@
     1.4    with Step prems show "P a s" by simp
     1.5  qed
     1.6  
     1.7 -lemmas smap_simps[simp] = stream.sel_map
     1.8 -lemmas shd_sset = stream.sel_set(1)
     1.9 -lemmas stl_sset = stream.sel_set(2)
    1.10 +lemmas smap_simps[simp] = stream.map_sel
    1.11 +lemmas shd_sset = stream.set_sel(1)
    1.12 +lemmas stl_sset = stream.set_sel(2)
    1.13  
    1.14  (* only for the non-mutual case: *)
    1.15  theorem sset_induct1[consumes 1, case_names shd stl, induct set: "sset"]: