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