src/HOL/Predicate.thy
changeset 31216 29da4d396e1f
parent 31133 a9f728dc5c8e
child 31222 4a84ae57b65f
     1.1 --- a/src/HOL/Predicate.thy	Wed May 20 15:35:22 2009 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Wed May 20 22:24:07 2009 +0200
     1.3 @@ -627,6 +627,9 @@
     1.4  lemma eq_is_eq: "eq x y \<equiv> (x = y)"
     1.5    by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
     1.6  
     1.7 +definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where
     1.8 +  "map f P = P \<guillemotright>= (single o f)"
     1.9 +
    1.10  ML {*
    1.11  signature PREDICATE =
    1.12  sig
    1.13 @@ -683,7 +686,7 @@
    1.14  val _ = OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
    1.15    OuterKeyword.thy_goal (P.term_group >> (K (Proof.theorem_i NONE (K I) [[]])));
    1.16  
    1.17 -val _ = OuterSyntax.improper_command "values" "evaluate and print enumerations"
    1.18 +val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions"
    1.19    OuterKeyword.diag ((opt_modes -- P.term)
    1.20      >> (fn (modes, t) => Toplevel.no_timing o Toplevel.keep
    1.21          (K ())));
    1.22 @@ -702,6 +705,6 @@
    1.23  
    1.24  hide (open) type pred seq
    1.25  hide (open) const Pred eval single bind if_pred not_pred
    1.26 -  Empty Insert Join Seq member pred_of_seq "apply" adjunct eq
    1.27 +  Empty Insert Join Seq member pred_of_seq "apply" adjunct eq map
    1.28  
    1.29  end