# HG changeset patch
# User haftmann
# Date 1245075199 -7200
# Node ID b040f1679f770cc0a7cfb5a918cbe27e09d9c753
# Parent  ce68241f711f4992e518bcba98574e6576463b65
authentic syntax for Pow and image

diff -r ce68241f711f -r b040f1679f77 NEWS
--- a/NEWS	Mon Jun 15 16:13:04 2009 +0200
+++ b/NEWS	Mon Jun 15 16:13:19 2009 +0200
@@ -40,6 +40,9 @@
 * Implementation of quickcheck using generic code generator; default generators
 are provided for all suitable HOL types, records and datatypes.
 
+* Constants Set.Pow and Set.image now with authentic syntax; object-logic definitions
+Set.Pow_def and Set.image_def.  INCOMPATIBILITY.
+
 
 *** ML ***
 
diff -r ce68241f711f -r b040f1679f77 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Jun 15 16:13:04 2009 +0200
+++ b/src/HOL/Set.thy	Mon Jun 15 16:13:19 2009 +0200
@@ -23,8 +23,6 @@
   Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
   Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
   Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
-  Pow           :: "'a set => 'a set set"                -- "powerset"
-  image         :: "('a => 'b) => 'a set => 'b set"      (infixr "`" 90)
 
 local
 
@@ -215,9 +213,6 @@
   supset_eq  ("op \<supseteq>") and
   supset_eq  ("(_/ \<supseteq> _)" [50, 51] 50)
 
-abbreviation
-  range :: "('a => 'b) => 'b set" where -- "of function"
-  "range f == f ` UNIV"
 
 
 subsubsection "Bounded quantifiers"
@@ -408,9 +403,15 @@
 
 end
 
-defs
-  Pow_def:      "Pow A          == {B. B <= A}"
-  image_def:    "f`A            == {y. EX x:A. y = f(x)}"
+definition Pow :: "'a set => 'a set set" where
+  Pow_def: "Pow A = {B. B \<le> A}"
+
+definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where
+  image_def: "f ` A = {y. EX x:A. y = f(x)}"
+
+abbreviation
+  range :: "('a => 'b) => 'b set" where -- "of function"
+  "range f == f ` UNIV"
 
 
 subsection {* Lemmas and proof tool setup *}
diff -r ce68241f711f -r b040f1679f77 src/HOL/Tools/datatype_package/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Mon Jun 15 16:13:04 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Mon Jun 15 16:13:19 2009 +0200
@@ -458,9 +458,9 @@
       let val isoT = T --> Univ_elT
       in HOLogic.imp $ 
         (Const (set_name, UnivT') $ mk_Free "x" Univ_elT i) $
-          (if i < length newTs then Const ("True", HOLogic.boolT)
+          (if i < length newTs then HOLogic.true_const
            else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
-             Const ("image", [isoT, HOLogic.mk_setT T] ---> UnivT) $
+             Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $
                Const (iso_name, isoT) $ Const (@{const_name UNIV}, HOLogic.mk_setT T)))
       end;