# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1333516778 -3600
# Node ID da59c94bed7e8ad32b752f08e95f0c5fdb887d48
# Parent  16e6140225afc930ca4a9c4b1362d99451ae128a
updated to Isabelle version April 1

diff -r 16e6140225af -r da59c94bed7e Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Tue Apr 03 23:09:13 2012 +0100
+++ b/Nominal/Nominal2_Abs.thy	Wed Apr 04 06:19:38 2012 +0100
@@ -470,21 +470,21 @@
 where
   "Abs_set::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_set"
 is
-  "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
+  "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" .
 
 quotient_definition
   Abs_res ("[_]res. _" [60, 60] 60)
 where
   "Abs_res::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_res"
 is
-  "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
+  "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" .
 
 quotient_definition
   Abs_lst ("[_]lst. _" [60, 60] 60)
 where
   "Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst"
 is
-  "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)"
+  "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)" .
 
 lemma [quot_respect]:
   shows "(op= ===> op= ===> alpha_abs_set) Pair Pair"
@@ -540,7 +540,8 @@
 quotient_definition
   "permute_abs_set::perm \<Rightarrow> ('a::pt abs_set) \<Rightarrow> 'a abs_set"
 is
-  "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
+  "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)" 
+  by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
 
 lemma permute_Abs_set[simp]:
   fixes x::"'a::pt"  
@@ -562,6 +563,7 @@
   "permute_abs_res::perm \<Rightarrow> ('a::pt abs_res) \<Rightarrow> 'a abs_res"
 is
   "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
+  by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
 
 lemma permute_Abs_res[simp]:
   fixes x::"'a::pt"  
@@ -583,6 +585,7 @@
   "permute_abs_lst::perm \<Rightarrow> ('a::pt abs_lst) \<Rightarrow> 'a abs_lst"
 is
   "permute:: perm \<Rightarrow> (atom list \<times> 'a::pt) \<Rightarrow> (atom list \<times> 'a::pt)"
+  by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
 
 lemma permute_Abs_lst[simp]:
   fixes x::"'a::pt"  
diff -r 16e6140225af -r da59c94bed7e Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Tue Apr 03 23:09:13 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Wed Apr 04 06:19:38 2012 +0100
@@ -629,6 +629,7 @@
   "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is
   "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  by (simp add: set_eqvt[symmetric])
 
 instance 
 proof