# HG changeset patch
# User nipkow
# Date 1113214707 -7200
# Node ID f072119afa4ede5f12eb6a87b99063b3602e323a
# Parent  3c49dbece0a8077af3c63004c0db6df5786b1e0d
tuned

diff -r 3c49dbece0a8 -r f072119afa4e src/HOL/Map.thy
--- 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"