equal
deleted
inserted
replaced
41 ML {* |
41 ML {* |
42 open Quotient_Term; |
42 open Quotient_Term; |
43 *} |
43 *} |
44 |
44 |
45 ML {* |
45 ML {* |
46 get_fun absF @{context} (@{typ "'a list"}, |
46 absrep_fun absF @{context} (@{typ "'a list"}, |
47 @{typ "'a fset"}) |
47 @{typ "'a fset"}) |
48 |> Syntax.check_term @{context} |
48 |> Syntax.check_term @{context} |
49 |> Syntax.string_of_term @{context} |
49 |> Syntax.string_of_term @{context} |
50 |> writeln |
50 |> writeln |
51 *} |
51 *} |
52 |
52 |
53 term "map id" |
53 term "map id" |
54 term "abs_fset o (map id)" |
54 term "abs_fset o (map id)" |
55 |
55 |
56 ML {* |
56 ML {* |
57 get_fun absF @{context} (@{typ "(nat * nat) list"}, |
57 absrep_fun absF @{context} (@{typ "(nat * nat) list"}, |
58 @{typ "int fset"}) |
58 @{typ "int fset"}) |
59 |> Syntax.check_term @{context} |
59 |> Syntax.check_term @{context} |
60 |> Syntax.string_of_term @{context} |
60 |> Syntax.string_of_term @{context} |
61 |> writeln |
61 |> writeln |
62 *} |
62 *} |
64 term "map abs_int" |
64 term "map abs_int" |
65 term "abs_fset o map abs_int" |
65 term "abs_fset o map abs_int" |
66 |
66 |
67 |
67 |
68 ML {* |
68 ML {* |
69 get_fun absF @{context} (@{typ "('a list) list"}, |
69 absrep_fun absF @{context} (@{typ "('a list) list"}, |
70 @{typ "('a fset) fset"}) |
70 @{typ "('a fset) fset"}) |
71 |> Syntax.check_term @{context} |
71 |> Syntax.check_term @{context} |
72 |> Syntax.string_of_term @{context} |
72 |> Syntax.string_of_term @{context} |
73 |> writeln |
73 |> writeln |
74 *} |
74 *} |
75 |
75 |
76 ML {* |
76 ML {* |
77 get_fun absF @{context} (@{typ "('a list) list \<Rightarrow> 'a"}, |
77 absrep_fun absF @{context} (@{typ "('a list) list \<Rightarrow> 'a"}, |
78 @{typ "('a fset) fset \<Rightarrow> 'a"}) |
78 @{typ "('a fset) fset \<Rightarrow> 'a"}) |
79 |> Syntax.check_term @{context} |
79 |> Syntax.check_term @{context} |
80 |> Syntax.string_of_term @{context} |
80 |> Syntax.string_of_term @{context} |
81 |> writeln |
81 |> writeln |
82 *} |
82 *} |