--- a/NEWS Sat Sep 23 16:02:01 2000 +0200
+++ b/NEWS Sat Sep 23 16:08:23 2000 +0200
@@ -45,6 +45,8 @@
* HOL: the constant for "f``x" is now "image" rather than "op ``";
+* HOL: the constant for "f-``x" is now "vimage" rather than "op -``";
+
* HOL: the disjoint sum is now "<+>" instead of "Plus"; the cartesian
product is now "<*>" instead of "Times"; the lexicographic product is
now "<*lex*>" instead of "**";
--- a/src/HOL/Tools/inductive_package.ML Sat Sep 23 16:02:01 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML Sat Sep 23 16:08:23 2000 +0200
@@ -185,7 +185,7 @@
val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD);
-val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op -``";
+val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "vimage";
val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
(* make injections needed in mutually recursive definitions *)
--- a/src/HOL/Vimage.thy Sat Sep 23 16:02:01 2000 +0200
+++ b/src/HOL/Vimage.thy Sat Sep 23 16:08:23 2000 +0200
@@ -8,10 +8,8 @@
Vimage = Set +
-consts
- "-``" :: ['a => 'b, 'b set] => ('a set) (infixr 90)
-
-defs
- vimage_def "f-``B == {x. f(x) : B}"
+constdefs
+ vimage :: ['a => 'b, 'b set] => ('a set) (infixr "-``" 90)
+ "f-``B == {x. f(x) : B}"
end