# HG changeset patch
# User urbanc
# Date 1130885753 -3600
# Node ID 2719a6b7d95e6ee33ffbafe512e27e98f651ec43
# Parent  004515accc10754eb152413e9701acd9a6f3c6df
some minor tweaks in some proofs (nothing extraordinary)

diff -r 004515accc10 -r 2719a6b7d95e src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Tue Nov 01 23:54:29 2005 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Tue Nov 01 23:55:53 2005 +0100
@@ -293,9 +293,9 @@
   case Nil show ?case by (simp add: at1[OF at])
 next
   case (Cons x xs)
-  assume i: "(xs @ pi2)\<bullet>c  =  xs\<bullet>(pi2\<bullet>c)"
-  have "(x#xs)@pi2 = x#(xs@pi2)" by simp
-  thus ?case using i by (cases "x", simp add:  at2[OF at])
+  have "(xs@pi2)\<bullet>c  =  xs\<bullet>(pi2\<bullet>c)" by fact
+  also have "(x#xs)@pi2 = x#(xs@pi2)" by simp
+  ultimately show ?case by (cases "x", simp add:  at2[OF at])
 qed
  
 lemma at_swap:
@@ -551,7 +551,7 @@
 apply(auto simp only: pt_def)
 apply(simp only: at1[OF at])
 apply(simp only: at_append[OF at]) 
-apply(simp add: prm_eq_def)
+apply(simp only: prm_eq_def)
 done
 
 section {* finite support properties *}
@@ -895,7 +895,7 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "((pi\<bullet>x)\<in>(pi\<bullet>X)) = (x\<in>X)"
-  by (simp add: perm_set_def pt_set_bij1[OF pt, OF at] pt_bij[OF pt, OF at])
+  by (simp add: perm_set_def pt_bij[OF pt, OF at])
 
 lemma pt_set_bij2:
   fixes pi :: "'x prm"
@@ -1266,7 +1266,7 @@
   and   S1 :: "'x set"
   and   S2 :: "'x set"
   assumes  a: "S1 supports x"
-  and      b: "S1\<subseteq>S2"
+  and      b: "S1 \<subseteq> S2"
   shows "S2 supports x"
   using a b
   by (force simp add: "op supports_def")