summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Sat, 23 Sep 2000 16:08:23 +0200 | |

changeset 10065 | ddb3a014f721 |

parent 10064 | 1a77667b21ef |

child 10066 | 2f5686cf8c9a |

renaming the inverse image operator in HOL

NEWS | file | annotate | diff | comparison | revisions | |

src/HOL/Tools/inductive_package.ML | file | annotate | diff | comparison | revisions | |

src/HOL/Vimage.thy | file | annotate | diff | comparison | revisions |

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