src/HOL/Map.thy
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"