src/HOL/Map.thy
changeset 15695 f072119afa4e
parent 15693 3a67e61c6e96
child 17391 c6338ed6caf8
     1.1 --- a/src/HOL/Map.thy	Mon Apr 11 12:14:48 2005 +0200
     1.2 +++ b/src/HOL/Map.thy	Mon Apr 11 12:18:27 2005 +0200
     1.3 @@ -63,7 +63,8 @@
     1.4  					  ("_/'(_/\<mapsto>\<lambda>_. _')"  [900,0,0,0] 900)
     1.5  
     1.6  syntax (latex output)
     1.7 -  restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110) --"requires amssymb!"
     1.8 +  restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
     1.9 +  --"requires amssymb!"
    1.10  
    1.11  translations
    1.12    "empty"    => "_K None"