# HG changeset patch
# User paulson
# Date 969718103 -7200
# Node ID ddb3a014f7216584a9937fd80307bc0fd12f392f
# Parent  1a77667b21ef896ec614df3441063524c50f44ab
renaming the inverse image operator in HOL

diff -r 1a77667b21ef -r ddb3a014f721 NEWS
--- 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 "**";
diff -r 1a77667b21ef -r ddb3a014f721 src/HOL/Tools/inductive_package.ML
--- 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 *)
diff -r 1a77667b21ef -r ddb3a014f721 src/HOL/Vimage.thy
--- 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