# HG changeset patch
# User nipkow
# Date 1285167141 -7200
# Node ID 3810834690c46faabb7a43d2ef9ea46ca1ec6a13
# Parent  106e8952fd2884048a4bf7a326eb1708f6b9d211# Parent  7723505c746a97b341900a846893b7c59ea84236
merged

diff -r 106e8952fd28 -r 3810834690c4 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Sep 22 16:24:41 2010 +0200
+++ b/src/HOL/List.thy	Wed Sep 22 16:52:21 2010 +0200
@@ -4157,8 +4157,8 @@
   lists :: "'a set => 'a list set"
   for A :: "'a set"
 where
-    Nil [intro!]: "[]: lists A"
-  | Cons [intro!,no_atp]: "[| a: A; l: lists A|] ==> a#l : lists A"
+    Nil [intro!, simp]: "[]: lists A"
+  | Cons [intro!, simp, no_atp]: "[| a: A; l: lists A|] ==> a#l : lists A"
 
 inductive_cases listsE [elim!,no_atp]: "x#l : lists A"
 inductive_cases listspE [elim!,no_atp]: "listsp A (x # l)"
@@ -4184,6 +4184,9 @@
 
 lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]
 
+lemma Cons_in_lists_iff[simp]: "x#xs : lists A \<longleftrightarrow> x:A \<and> xs : lists A"
+by auto
+
 lemma append_in_listsp_conv [iff]:
      "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
 by (induct xs) auto
@@ -4209,6 +4212,9 @@
 lemma lists_eq_set: "lists A = {xs. set xs <= A}"
 by auto
 
+lemma lists_empty [simp]: "lists {} = {[]}"
+by auto
+
 lemma lists_UNIV [simp]: "lists UNIV = UNIV"
 by auto
 
diff -r 106e8952fd28 -r 3810834690c4 src/HOL/Nominal/Examples/Standardization.thy
--- a/src/HOL/Nominal/Examples/Standardization.thy	Wed Sep 22 16:24:41 2010 +0200
+++ b/src/HOL/Nominal/Examples/Standardization.thy	Wed Sep 22 16:52:21 2010 +0200
@@ -654,7 +654,6 @@
   shows "listsp ((pi::name prm) \<bullet> p) (pi \<bullet> xs)" using xs
   apply induct
   apply simp
-  apply (rule listsp.intros)
   apply simp
   apply (rule listsp.intros)
   apply (drule_tac pi=pi in perm_boolI)
diff -r 106e8952fd28 -r 3810834690c4 src/HOL/Proofs/Lambda/StrongNorm.thy
--- a/src/HOL/Proofs/Lambda/StrongNorm.thy	Wed Sep 22 16:24:41 2010 +0200
+++ b/src/HOL/Proofs/Lambda/StrongNorm.thy	Wed Sep 22 16:52:21 2010 +0200
@@ -24,7 +24,6 @@
        rule IT.Var,
        erule listsp.induct,
        simp (no_asm),
-       rule listsp.Nil,
        simp (no_asm),
        rule listsp.Cons,
        blast,
@@ -44,7 +43,6 @@
       rule IT.Var,
       erule listsp.induct,
       simp (no_asm),
-      rule listsp.Nil,
       simp (no_asm),
       rule listsp.Cons,
       fast,