src/ZF/List_ZF.thy
changeset 58860 fee7cfa69c50
parent 46953 2b6e55924af3
child 58871 c399ae4b836f
     1.1 --- a/src/ZF/List_ZF.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/ZF/List_ZF.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -1216,7 +1216,7 @@
     1.4  lemma sublist_upt_eq_take [rule_format, simp]:
     1.5      "xs:list(A) ==> \<forall>n\<in>nat. sublist(xs,n) = take(n,xs)"
     1.6  apply (erule list.induct, simp)
     1.7 -apply (clarify );
     1.8 +apply (clarify )
     1.9  apply (erule natE)
    1.10  apply (simp_all add: nat_eq_Collect_lt Ord_mem_iff_lt sublist_Cons)
    1.11  done