# HG changeset patch
# User haftmann
# Date 1242851047 -7200
# Node ID 29da4d396e1f7e08c1c6d03a5e573f36299d4fec
# Parent  052fddd640066736c65f4d6bf41762eefecf07bf
added Predicate.map

diff -r 052fddd64006 -r 29da4d396e1f src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed May 20 15:35:22 2009 +0200
+++ b/src/HOL/Predicate.thy	Wed May 20 22:24:07 2009 +0200
@@ -627,6 +627,9 @@
 lemma eq_is_eq: "eq x y \<equiv> (x = y)"
   by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
 
+definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where
+  "map f P = P \<guillemotright>= (single o f)"
+
 ML {*
 signature PREDICATE =
 sig
@@ -683,7 +686,7 @@
 val _ = OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
   OuterKeyword.thy_goal (P.term_group >> (K (Proof.theorem_i NONE (K I) [[]])));
 
-val _ = OuterSyntax.improper_command "values" "evaluate and print enumerations"
+val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions"
   OuterKeyword.diag ((opt_modes -- P.term)
     >> (fn (modes, t) => Toplevel.no_timing o Toplevel.keep
         (K ())));
@@ -702,6 +705,6 @@
 
 hide (open) type pred seq
 hide (open) const Pred eval single bind if_pred not_pred
-  Empty Insert Join Seq member pred_of_seq "apply" adjunct eq
+  Empty Insert Join Seq member pred_of_seq "apply" adjunct eq map
 
 end