# HG changeset patch
# User wenzelm
# Date 1296755862 -3600
# Node ID 19890332febc3e66a2afa43da449b98763871d2f
# Parent  f69bb9077b02f97238f987252f438e73d69ded56
explicit is better than implicit;

diff -r f69bb9077b02 -r 19890332febc src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Feb 02 22:48:24 2011 +0100
+++ b/src/HOL/List.thy	Thu Feb 03 18:57:42 2011 +0100
@@ -456,7 +456,9 @@
   "xs \<noteq> x # xs"
 by (induct xs) auto
 
-lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric]
+lemma not_Cons_self2 [simp]:
+  "x # xs \<noteq> xs"
+by (rule not_Cons_self [symmetric])
 
 lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)"
 by (induct xs) auto