--- 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