# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268759614 -3600
# Node ID c79bcbe1983d555c5222782545c689d60fe451be
# Parent  0fd03936dedb46641ab6af7dcbd9a95a9621232e
added the final unfolded result

diff -r 0fd03936dedb -r c79bcbe1983d Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 16 18:02:08 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 16 18:13:34 2010 +0100
@@ -43,8 +43,8 @@
   by (rule eqvts)
 
 lemma supp_fv:
-  "supp t = fv_lam t" and 
-  "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}"
+  shows "supp t = fv_lam t" 
+  and "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}"
 apply(induct t and bp rule: lam_bp_inducts)
 apply(simp_all add: lam_bp_fv)
 (* VAR case *)
@@ -107,6 +107,8 @@
 apply(blast)
 done
 
+thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
+
 text {* example 2 *}
 
 nominal_datatype trm' =