FSet.thy
changeset 212 ca9eae5bd871
parent 202 8ca1150f34d0
child 213 7610d2bbca48
--- a/FSet.thy	Tue Oct 27 14:46:38 2009 +0100
+++ b/FSet.thy	Wed Oct 28 01:48:45 2009 +0100
@@ -168,7 +168,8 @@
 thm fold_def
 
 local_setup {*
-  make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn 
+  @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term map
@@ -176,6 +177,8 @@
 thm fmap_def
 
 
+
+
 ML {*
   val consts = [@{const_name "Nil"}, @{const_name "Cons"},
                 @{const_name "membship"}, @{const_name "card1"},