recovered HOL-Proofs-Lambda from 8aedca31957d: avoid problems with program extraction according to d136af442665;
authorwenzelm
Sat Aug 04 16:21:25 2018 +0200 (11 months ago)
changeset 6872360611540bcff
parent 68722 6aea897bff2a
child 68724 7fafadbf16c7
recovered HOL-Proofs-Lambda from 8aedca31957d: avoid problems with program extraction according to d136af442665;
src/HOL/List.thy
     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