--- a/QuotMain.thy Sat Oct 24 14:00:18 2009 +0200
+++ b/QuotMain.thy Sat Oct 24 16:09:05 2009 +0200
@@ -158,6 +158,12 @@
use "quotient.ML"
(* mapfuns for some standard types *)
+setup {*
+ maps_update @{type_name "list"} {mapfun = @{const_name "map"}, relfun = @{const_name "LIST_REL"}} #>
+ maps_update @{type_name "*"} {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #>
+ maps_update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}}
+*}
+
ML {* quotdata_lookup @{theory} *}
setup {* quotdata_update_thy (@{typ nat}, @{typ bool}, @{term "True"})*}