# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271932935 -7200
# Node ID 99367d481f7859b2fd096894e47b5a97ccc302cd
# Parent  266abc3ee228258745d4b71c010f79e674f6752f
Converted 'thm' to a lemma.

diff -r 266abc3ee228 -r 99367d481f78 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Thu Apr 22 12:33:51 2010 +0200
+++ b/Nominal/FSet.thy	Thu Apr 22 12:42:15 2010 +0200
@@ -1070,7 +1070,8 @@
   "(finsert x xs |\<subseteq>| ys) = (x |\<in>| ys \<and> xs |\<subseteq>| ys)"
   by (lifting sub_list_cons)
 
-thm sub_list_def[simplified memb_def[symmetric], quot_lifted, no_vars]
+lemma "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys"
+  by (lifting sub_list_def[simplified memb_def[symmetric]])
 
 lemma fsubset_fin: "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
 by (rule meta_eq_to_obj_eq)