equal
deleted
inserted
replaced
27 |
27 |
28 translations |
28 translations |
29 "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)" |
29 "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)" |
30 |
30 |
31 print_translation \<open> |
31 print_translation \<open> |
32 [(\<^const_syntax>\<open>Eps\<close>, fn _ => fn [Abs abs] => |
32 [(\<^const_syntax>\<open>Eps\<close>, fn ctxt => fn [Abs abs] => |
33 let val (x, t) = Syntax_Trans.atomic_abs_tr' abs |
33 let val (x, t) = Syntax_Trans.atomic_abs_tr' ctxt abs |
34 in Syntax.const \<^syntax_const>\<open>_Eps\<close> $ x $ t end)] |
34 in Syntax.const \<^syntax_const>\<open>_Eps\<close> $ x $ t end)] |
35 \<close> \<comment> \<open>to avoid eta-contraction of body\<close> |
35 \<close> \<comment> \<open>to avoid eta-contraction of body\<close> |
36 |
36 |
37 definition inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where |
37 definition inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where |
38 "inv_into A f = (\<lambda>x. SOME y. y \<in> A \<and> f y = x)" |
38 "inv_into A f = (\<lambda>x. SOME y. y \<in> A \<and> f y = x)" |