equal
deleted
inserted
replaced
226 @{const interp}. Note that values are represented by variable indices (@{typ nat}) |
226 @{const interp}. Note that values are represented by variable indices (@{typ nat}) |
227 whose concrete values are given in list @{term vs}. |
227 whose concrete values are given in list @{term vs}. |
228 \<close> |
228 \<close> |
229 |
229 |
230 ML (*<*) \<open>\<close> |
230 ML (*<*) \<open>\<close> |
231 schematic_lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P" |
231 schematic_goal "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P" |
232 ML_prf |
232 ML_prf |
233 (*>*) \<open>val thm = |
233 (*>*) \<open>val thm = |
234 Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*) |
234 Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*) |
235 by (tactic \<open>ALLGOALS (resolve_tac @{context} [thm])\<close>) |
235 by (tactic \<open>ALLGOALS (resolve_tac @{context} [thm])\<close>) |
236 (*>*) |
236 (*>*) |