src/HOL/Map.thy
changeset 13914 026866537fae
parent 13912 3c0a340be514
child 13937 e9d57517c9b1
     1.1 --- a/src/HOL/Map.thy	Wed Apr 16 22:14:08 2003 +0200
     1.2 +++ b/src/HOL/Map.thy	Wed Apr 16 22:21:32 2003 +0200
     1.3 @@ -6,6 +6,8 @@
     1.4  The datatype of `maps' (written ~=>); strongly resembles maps in VDM.
     1.5  *)
     1.6  
     1.7 +header {* Maps *}
     1.8 +
     1.9  theory Map = List:
    1.10  
    1.11  types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)