removed "symbols" syntax for constant "override";
authorwenzelm
Tue Oct 03 18:40:25 2000 +0200 (2000-10-03)
changeset 10137d1c2bef01e2f
parent 10136 ed576de7bddc
child 10138 412a3ced6efd
removed "symbols" syntax for constant "override";
NEWS
src/HOL/Map.thy
     1.1 --- a/NEWS	Tue Oct 03 18:39:31 2000 +0200
     1.2 +++ b/NEWS	Tue Oct 03 18:40:25 2000 +0200
     1.3 @@ -55,6 +55,13 @@
     1.4  * HOL: theory Sexp is now in HOL/Induct examples (it used to be part
     1.5  of main HOL, but was unused); better use HOL's datatype package;
     1.6  
     1.7 +* HOL: removed "symbols" syntax for constant "override" of theory Map;
     1.8 +the old syntax may be recovered as follows:
     1.9 +
    1.10 +  syntax (symbols)
    1.11 +    override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
    1.12 +      (infixl "\\<oplus>" 100)
    1.13 +
    1.14  * HOL/Real: "rabs" replaced by overloaded "abs" function;
    1.15  
    1.16  * HOL/ML: even fewer consts are declared as global (see theories Ord,
     2.1 --- a/src/HOL/Map.thy	Tue Oct 03 18:39:31 2000 +0200
     2.2 +++ b/src/HOL/Map.thy	Tue Oct 03 18:40:25 2000 +0200
     2.3 @@ -29,8 +29,6 @@
     2.4  					  ("_/'(_/\\<mapsto>/_')"  [900,0,0]900)
     2.5    map_upds  :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
     2.6  				         ("_/'(_/[\\<mapsto>]/_')" [900,0,0]900)
     2.7 -  override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
     2.8 -				         (infixl "\\<oplus>" 100)
     2.9  
    2.10  translations
    2.11