--- 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)