# HG changeset patch
# User wenzelm
# Date 970591225 -7200
# Node ID d1c2bef01e2f81859a45c881ec1fa88723ead6c7
# Parent  ed576de7bddc183013386ba655cbe114d14e018d
removed "symbols" syntax for constant "override";

diff -r ed576de7bddc -r d1c2bef01e2f NEWS
--- a/NEWS	Tue Oct 03 18:39:31 2000 +0200
+++ b/NEWS	Tue Oct 03 18:40:25 2000 +0200
@@ -55,6 +55,13 @@
 * HOL: theory Sexp is now in HOL/Induct examples (it used to be part
 of main HOL, but was unused); better use HOL's datatype package;
 
+* HOL: removed "symbols" syntax for constant "override" of theory Map;
+the old syntax may be recovered as follows:
+
+  syntax (symbols)
+    override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
+      (infixl "\\<oplus>" 100)
+
 * HOL/Real: "rabs" replaced by overloaded "abs" function;
 
 * HOL/ML: even fewer consts are declared as global (see theories Ord,
diff -r ed576de7bddc -r d1c2bef01e2f src/HOL/Map.thy
--- a/src/HOL/Map.thy	Tue Oct 03 18:39:31 2000 +0200
+++ b/src/HOL/Map.thy	Tue Oct 03 18:40:25 2000 +0200
@@ -29,8 +29,6 @@
 					  ("_/'(_/\\<mapsto>/_')"  [900,0,0]900)
   map_upds  :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
 				         ("_/'(_/[\\<mapsto>]/_')" [900,0,0]900)
-  override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
-				         (infixl "\\<oplus>" 100)
 
 translations