tuned
authornipkow
Mon Apr 11 12:18:27 2005 +0200 (2005-04-11)
changeset 15695f072119afa4e
parent 15694 3c49dbece0a8
child 15696 1da4ce092c0b
tuned
src/HOL/Map.thy
     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"