--- a/FSet.thy Sat Oct 24 14:00:18 2009 +0200
+++ b/FSet.thy Sat Oct 24 16:09:05 2009 +0200
@@ -14,18 +14,11 @@
quotient qt = "t" / "Rt"
by (rule t_eq)
-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 {*
get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
|> fst
|> Syntax.string_of_term @{context}
- |> writeln
+ |> writeln*)
*}
ML {*