src/HOL/Map.thy
changeset 63648 f9f3006a5579
parent 62390 842917225d56
child 63828 ca467e73f912
     1.1 --- a/src/HOL/Map.thy	Tue Aug 09 23:29:54 2016 +0200
     1.2 +++ b/src/HOL/Map.thy	Wed Aug 10 09:33:54 2016 +0200
     1.3 @@ -312,7 +312,7 @@
     1.4  apply (induct xs)
     1.5   apply simp
     1.6  apply (rule ext)
     1.7 -apply (simp split add: option.split)
     1.8 +apply (simp split: option.split)
     1.9  done
    1.10  
    1.11  lemma finite_range_map_of_map_add: