equal
deleted
inserted
replaced
25 |
25 |
26 syntax "_finite_cart" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15) |
26 syntax "_finite_cart" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15) |
27 |
27 |
28 parse_translation {* |
28 parse_translation {* |
29 let |
29 let |
30 fun cart t u = Syntax.const @{type_name cart} $ t $ u |
30 fun cart t u = Syntax.const @{type_name cart} $ t $ u; (* FIXME @{type_syntax} *) |
31 fun finite_cart_tr [t, u as Free (x, _)] = |
31 fun finite_cart_tr [t, u as Free (x, _)] = |
32 if Syntax.is_tid x |
32 if Syntax.is_tid x then |
33 then cart t (Syntax.const "_ofsort" $ u $ Syntax.const (hd @{sort finite})) |
33 cart t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const (hd @{sort finite})) |
34 else cart t u |
34 else cart t u |
35 | finite_cart_tr [t, u] = cart t u |
35 | finite_cart_tr [t, u] = cart t u |
36 in |
36 in |
37 [("_finite_cart", finite_cart_tr)] |
37 [(@{syntax_const "_finite_cart"}, finite_cart_tr)] |
38 end |
38 end |
39 *} |
39 *} |
40 |
40 |
41 lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)" |
41 lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)" |
42 apply auto |
42 apply auto |