src/HOL/List.thy
changeset 68723 60611540bcff
parent 68719 8aedca31957d
child 68775 8fbfb67f6824
     1.1 --- a/src/HOL/List.thy	Sat Aug 04 15:49:54 2018 +0200
     1.2 +++ b/src/HOL/List.thy	Sat Aug 04 16:21:25 2018 +0200
     1.3 @@ -1242,7 +1242,7 @@
     1.4  
     1.5  lemma rev_induct [case_names Nil snoc]:
     1.6    "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
     1.7 -apply(subst rev_rev_ident[symmetric])
     1.8 +apply(simplesubst rev_rev_ident[symmetric])
     1.9  apply(rule_tac list = "rev xs" in list.induct, simp_all)
    1.10  done
    1.11