diff -r a6f3e1b08494 -r b6873d123f9b Attic/Quot/Examples/FSet_BallBex.thy
--- a/Attic/Quot/Examples/FSet_BallBex.thy	Sat May 12 21:05:59 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-theory FSet_ballbex
-imports "../../../Nominal/FSet"
-begin
-
-notation
-  list_eq (infix "\<approx>" 50)
-
-lemma test:
-  "\<forall>xs \<in> (\<lambda>xs. memb x xs). memb x (y # xs)"
-  apply (simp add: memb_def)
-  apply (metis mem_def)
-  done
-
-thm test[quot_lifted]
-
-lemma "\<forall>xs \<in> (\<lambda>xs. x |\<in>| xs). x |\<in>| finsert y xs"
-  unfolding Ball_def
-  by (lifting test[unfolded Ball_def])
-
-ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Ball_def Bex_def} @{thm test}*}
-
-lemma test2:
-  "\<exists>xs \<in> (\<lambda>xs. xs \<approx> []). xs \<approx> []"
-  apply (rule_tac x="[]" in bexI)
-  apply (auto simp add: mem_def)
-  done
-
-thm test2[quot_lifted]
-
-lemma "\<exists>xs \<in> (\<lambda>xs. xs = {||}). xs = {||}"
-  unfolding Bex_def
-  by (lifting test2[unfolded Bex_def])
-
-ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Bex_def} @{thm test2}*}
-
-end