src/HOL/Corec_Examples/LFilter.thy
changeset 62698 9d706e37ddab
parent 62694 f50d7efc8fe3
child 62726 5b2a7caa855b
     1.1 --- a/src/HOL/Corec_Examples/LFilter.thy	Tue Mar 22 13:32:40 2016 +0100
     1.2 +++ b/src/HOL/Corec_Examples/LFilter.thy	Tue Mar 22 13:44:50 2016 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4    show "x \<in> lset xs \<inter> {x. P x}" if "x \<in> lset (lfilter P xs)" for x using that
     1.5    proof(induction ys\<equiv>"lfilter P xs" arbitrary: xs rule: llist.set_induct)
     1.6      case (LCons1 x xs ys)
     1.7 -    from this show ?case 
     1.8 +    from this show ?case
     1.9        apply(induction arg\<equiv>"(P, ys)" arbitrary: ys rule: lfilter.inner_induct)
    1.10        subgoal by(subst (asm) (2) lfilter.code)(auto split: if_split_asm elim: llist.set_cases)
    1.11        done
    1.12 @@ -94,7 +94,7 @@
    1.13        apply auto
    1.14        done
    1.15    qed
    1.16 -qed   
    1.17 +qed
    1.18  
    1.19  lemma lfilter_lfilter: "lfilter P \<circ> lfilter Q = lfilter (\<lambda>x. P x \<and> Q x)"
    1.20    by(rule lfilter_unique)(auto elim: llist.set_cases)