# HG changeset patch
# User nipkow
# Date 1050524492 -7200
# Node ID 026866537faeb953d6ff5ec05a4e64207ea3f299
# Parent  b3ed67af04b8d4c12425f22cf471186c482bf0ee
header

diff -r b3ed67af04b8 -r 026866537fae src/HOL/Map.thy
--- a/src/HOL/Map.thy	Wed Apr 16 22:14:08 2003 +0200
+++ b/src/HOL/Map.thy	Wed Apr 16 22:21:32 2003 +0200
@@ -6,6 +6,8 @@
 The datatype of `maps' (written ~=>); strongly resembles maps in VDM.
 *)
 
+header {* Maps *}
+
 theory Map = List:
 
 types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)