# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271226931 -7200
# Node ID 2ccc1b00377c187620cf0cad9ee8ae37aed5782b
# Parent  91ba55dba5e024569f3e8c7eb553e138c77401c3
merge part1: none_memb_nil

diff -r 91ba55dba5e0 -r 2ccc1b00377c Nominal/FSet.thy
--- a/Nominal/FSet.thy	Wed Apr 14 08:16:54 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 14 08:35:31 2010 +0200
@@ -245,9 +245,9 @@
   "x # x # xs \<approx> x # xs"
   by auto
 
-lemma none_mem_nil:
-  "(\<forall>x. x \<notin> set xs) = (xs \<approx> [])"
-  by simp
+lemma none_memb_nil:
+  "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
+  by (simp add: memb_def)
 
 lemma fset_raw_strong_cases:
   "(xs = []) \<or> (\<exists>x ys. ((\<not> memb x ys) \<and> (xs \<approx> x # ys)))"
@@ -339,7 +339,7 @@
 lemma ffold_raw_rsp_pre:
   "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
   apply (induct a arbitrary: b)
-  apply (simp add: hd_in_set memb_absorb memb_def none_mem_nil)
+  apply (simp add: hd_in_set memb_absorb memb_def none_memb_nil)
   apply (simp add: ffold_raw.simps)
   apply (rule conjI)
   apply (rule_tac [!] impI)
@@ -486,8 +486,8 @@
   by (lifting memb_def[symmetric])
 
 lemma none_fin_fempty:
-  "(\<forall>x. x \<notin> fset_to_set S) = (S = {||})"
-  by (lifting none_mem_nil)
+  "(\<forall>x. x |\<notin>| S) = (S = {||})"
+  by (lifting none_memb_nil)
 
 lemma fset_cong:
   "(fset_to_set S = fset_to_set T) = (S = T)"