--- a/Nominal/FSet.thy	Mon Apr 19 15:28:57 2010 +0200
+++ b/Nominal/FSet.thy	Mon Apr 19 15:33:19 2010 +0200
@@ -29,25 +29,6 @@
 where
   "sub_list xs ys \<equiv> (\<forall>x. x \<in> set xs \<longrightarrow> x \<in> set ys)"
 
-lemma sub_list_cons:
-  "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
-  by (auto simp add: memb_def sub_list_def)
-
-lemma nil_not_cons:
-  shows "\<not> ([] \<approx> x # xs)"
-  and   "\<not> (x # xs \<approx> [])"
-  by auto
-
-lemma sub_list_rsp1: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list xs zs = sub_list ys zs"
-  by (simp add: sub_list_def)
-
-lemma sub_list_rsp2: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list zs xs = sub_list zs ys"
-  by (simp add: sub_list_def)
-
-lemma [quot_respect]:
-  "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
-  by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2)
-
 quotient_type
   'a fset = "'a list" / "list_eq"
 by (rule list_eq_equivp)
@@ -95,6 +76,11 @@
 
 section {* Augmenting an fset -- @{const finsert} *}
 
+lemma nil_not_cons:
+  shows "\<not> ([] \<approx> x # xs)"
+  and   "\<not> (x # xs \<approx> [])"
+  by auto
+
 lemma not_memb_nil:
   shows "\<not> memb x []"
   by (simp add: memb_def)
@@ -138,6 +124,22 @@
 is
   "op @"
 
+section {* sub_list *}
+
+lemma sub_list_cons:
+  "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
+  by (auto simp add: memb_def sub_list_def)
+
+lemma sub_list_rsp1: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list xs zs = sub_list ys zs"
+  by (simp add: sub_list_def)
+
+lemma sub_list_rsp2: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list zs xs = sub_list zs ys"
+  by (simp add: sub_list_def)
+
+lemma [quot_respect]:
+  "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
+  by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2)
+
 section {* Cardinality of finite sets *}
 
 fun