src/HOL/Map.thy
changeset 5183 89f162de39cf
parent 3981 b4f93a8da835
child 5195 277831ae7eac
     1.1 --- a/src/HOL/Map.thy	Fri Jul 24 13:02:01 1998 +0200
     1.2 +++ b/src/HOL/Map.thy	Fri Jul 24 13:03:20 1998 +0200
     1.3 @@ -37,8 +37,8 @@
     1.4  dom_def "dom(m) == {a. m a ~= None}"
     1.5  ran_def "ran(m) == {b. ? a. m a = Some b}"
     1.6  
     1.7 -primrec map_of list
     1.8 -"map_of [] = empty"
     1.9 -"map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
    1.10 +primrec
    1.11 +  "map_of [] = empty"
    1.12 +  "map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
    1.13  
    1.14  end