src/HOL/Limited_Sequence.thy
changeset 67091 1393c2340eec
parent 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Limited_Sequence.thy	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Limited_Sequence.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -171,8 +171,8 @@
     1.4  definition neg_not_seq :: "unit pos_dseq \<Rightarrow> unit neg_dseq"
     1.5  where
     1.6    "neg_not_seq x = (\<lambda>i. case Lazy_Sequence.yield (x i) of
     1.7 -    None => Lazy_Sequence.hb_single ()
     1.8 -  | Some ((), xq) => Lazy_Sequence.empty)"
     1.9 +    None \<Rightarrow> Lazy_Sequence.hb_single ()
    1.10 +  | Some ((), xq) \<Rightarrow> Lazy_Sequence.empty)"
    1.11  
    1.12  
    1.13  ML \<open>