src/HOL/Library/FinFun.thy
changeset 60565 b7ee41f72add
parent 60500 903bb1495239
child 60583 a645a0e6d790
     1.1 --- a/src/HOL/Library/FinFun.thy	Wed Jun 24 00:30:03 2015 +0200
     1.2 +++ b/src/HOL/Library/FinFun.thy	Wed Jun 24 21:26:03 2015 +0200
     1.3 @@ -1361,7 +1361,7 @@
     1.4      and [simp]: "sorted xs" "distinct xs" by simp_all
     1.5    show "xs = (if b = finfun_default f then remove1 a (finfun_to_list f) else insort_insert a (finfun_to_list f))"
     1.6    proof(cases "b = finfun_default f")
     1.7 -    case True [simp]
     1.8 +    case [simp]: True
     1.9      show ?thesis
    1.10      proof(cases "finfun_dom f $ a")
    1.11        case True