added Predicate.map in SML environment
authorhaftmann
Thu May 21 09:07:13 2009 +0200 (2009-05-21)
changeset 312224a84ae57b65f
parent 31218 fa54c1e614df
child 31223 87bde6b5f793
added Predicate.map in SML environment
src/HOL/Predicate.thy
     1.1 --- a/src/HOL/Predicate.thy	Wed May 20 22:24:07 2009 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Thu May 21 09:07:13 2009 +0200
     1.3 @@ -637,6 +637,7 @@
     1.4    and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq
     1.5    val yield: 'a pred -> ('a * 'a pred) option
     1.6    val yieldn: int -> 'a pred -> 'a list * 'a pred
     1.7 +  val map: ('a -> 'b) -> 'a pred -> 'b pred
     1.8  end;
     1.9  
    1.10  structure Predicate : PREDICATE =
    1.11 @@ -661,6 +662,8 @@
    1.12  
    1.13  fun yieldn P = anamorph yield P;
    1.14  
    1.15 +fun map f = @{code map} f;
    1.16 +
    1.17  end;
    1.18  *}
    1.19