--- a/Nominal/Test.thy	Wed Mar 17 09:57:54 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 17 10:34:25 2010 +0100
@@ -332,6 +332,43 @@
 thm t_tyS_induct
 thm t_tyS_distinct
 
+ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
+ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *}
+
+lemma supp_fv_t_tyS:
+  shows "supp T = fv_t T" 
+  and   "supp S = fv_tyS S"
+apply(induct T and S rule: t_tyS_inducts)
+apply(simp_all add: t_tyS_fv)
+(* VarTS case *)
+apply(simp only: supp_def)
+apply(simp only: t_tyS_perm)
+apply(simp only: t_tyS_inject)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base)
+(* FunTS case *)
+apply(simp only: supp_def)
+apply(simp only: t_tyS_perm)
+apply(simp only: t_tyS_inject)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
+(* All case *)
+apply(rule_tac t="supp (All fun t_raw)" and s="supp (Abs (atom ` fun) t_raw)" in subst)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: t_tyS_perm)
+apply(simp only: permute_ABS)
+apply(simp only: t_tyS_inject)
+apply(simp only: Abs_eq_iff)
+apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw)
+apply(simp only: alpha_gen)
+apply(simp only: supp_eqvt[symmetric])
+apply(simp only: eqvts)
+oops
+(*apply(simp only: supp_Abs)
+done*)
+
 (* example 1 from Terms.thy *)
 
 nominal_datatype trm1 =

--- a/Paper/Paper.thy	Wed Mar 17 09:57:54 2010 +0100
+++ b/Paper/Paper.thy	Wed Mar 17 10:34:25 2010 +0100
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../Quot/QuotMain"
+imports "../Nominal/Test"
 begin
 (*>*)