equal
deleted
inserted
replaced
21 local |
21 local |
22 |
22 |
23 val term_of_int_list = HOLogic.mk_list \<^typ>\<open>int\<close> |
23 val term_of_int_list = HOLogic.mk_list \<^typ>\<open>int\<close> |
24 o map (HOLogic.mk_number \<^typ>\<open>int\<close> o @{code integer_of_int}); |
24 o map (HOLogic.mk_number \<^typ>\<open>int\<close> o @{code integer_of_int}); |
25 |
25 |
26 fun raw_sort (ctxt, ct, ks) = Thm.mk_binop \<^cterm>\<open>Pure.eq :: int list \<Rightarrow> int list \<Rightarrow> prop\<close> |
26 fun raw_sort (ctxt, ct, ks) = |
27 ct (Thm.cterm_of ctxt (term_of_int_list ks)); |
27 \<^instantiate>\<open>x = ct and y = \<open>Thm.cterm_of ctxt (term_of_int_list ks)\<close> |
|
28 in cterm "x \<equiv> y" for x y :: "int list"\<close>; |
28 |
29 |
29 val (_, sort_oracle) = Context.>>> (Context.map_theory_result |
30 val (_, sort_oracle) = Context.>>> (Context.map_theory_result |
30 (Thm.add_oracle (\<^binding>\<open>sort\<close>, raw_sort))); |
31 (Thm.add_oracle (\<^binding>\<open>sort\<close>, raw_sort))); |
31 |
32 |
32 in |
33 in |