src/HOL/DSequence.thy
changeset 34953 a053ad2a7a72
parent 34948 2d5f2a9f7601
child 36024 c1ce2f60b0f2
     1.1 --- a/src/HOL/DSequence.thy	Wed Jan 20 18:02:22 2010 +0100
     1.2 +++ b/src/HOL/DSequence.thy	Wed Jan 20 18:08:08 2010 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4          None => None
     1.5        | Some zq => Some (Lazy_Sequence.append yq zq))))"
     1.6  
     1.7 -fun bind :: "'a dseq => ('a => 'b dseq) => 'b dseq"
     1.8 +definition bind :: "'a dseq => ('a => 'b dseq) => 'b dseq"
     1.9  where
    1.10    "bind x f = (%i pol. 
    1.11       if i = 0 then
    1.12 @@ -53,7 +53,7 @@
    1.13           None => None
    1.14         | Some xq => map_seq f xq i pol))"
    1.15  
    1.16 -fun union :: "'a dseq => 'a dseq => 'a dseq"
    1.17 +definition union :: "'a dseq => 'a dseq => 'a dseq"
    1.18  where
    1.19    "union x y = (%i pol. case (x i pol, y i pol) of
    1.20        (Some xq, Some yq) => Some (Lazy_Sequence.append xq yq)
    1.21 @@ -63,7 +63,7 @@
    1.22  where
    1.23    "if_seq b = (if b then single () else empty)"
    1.24  
    1.25 -fun not_seq :: "unit dseq => unit dseq"
    1.26 +definition not_seq :: "unit dseq => unit dseq"
    1.27  where
    1.28    "not_seq x = (%i pol. case x i (\<not>pol) of
    1.29      None => Some Lazy_Sequence.empty
    1.30 @@ -71,7 +71,7 @@
    1.31        None => Some (Lazy_Sequence.single ())
    1.32      | Some _ => Some (Lazy_Sequence.empty)))"
    1.33  
    1.34 -fun map :: "('a => 'b) => 'a dseq => 'b dseq"
    1.35 +definition map :: "('a => 'b) => 'a dseq => 'b dseq"
    1.36  where
    1.37    "map f g = (%i pol. case g i pol of
    1.38       None => None
    1.39 @@ -106,7 +106,7 @@
    1.40    Sequence.append Sequence.flat Sequence.map Sequence.bind Sequence.ifpred Sequence.not_seq
    1.41  *)
    1.42  hide (open) const empty single eval map_seq bind union if_seq not_seq map
    1.43 -hide (open) fact empty_def single_def eval.simps map_seq.simps bind.simps union.simps
    1.44 -  if_seq_def not_seq.simps map.simps
    1.45 +hide (open) fact empty_def single_def eval.simps map_seq.simps bind_def union_def
    1.46 +  if_seq_def not_seq_def map_def
    1.47  
    1.48  end