# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1287348023 -3600
# Node ID 8537493c039f89ed27e2ecb92b6877af4373af3f
# Parent  1f5c8e85c41fa5af05e7196acb766829498791d0
fixed typo

diff -r 1f5c8e85c41f -r 8537493c039f Nominal/FSet.thy
--- a/Nominal/FSet.thy	Sun Oct 17 15:53:37 2010 +0100
+++ b/Nominal/FSet.thy	Sun Oct 17 21:40:23 2010 +0100
@@ -9,7 +9,7 @@
 imports Quotient_List
 begin
 
-text {* Definiton of the equivalence relation over lists *}
+text {* Definition of the equivalence relation over lists *}
 
 fun
   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
@@ -523,9 +523,9 @@
 subsection {* fset *}
 
 lemma fset_simps [simp]:
-  "fset {||} = ({} :: 'a set)"
-  "fset (insert_fset (x :: 'a) S) = insert x (fset S)"
-  by (lifting set.simps)
+  shows "fset {||} = {}"
+  and   "fset (insert_fset x S) = insert x (fset S)"
+  by (descending, simp)+
 
 lemma finite_fset [simp]: 
   shows "finite (fset S)"