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