changeset 61337 | 4645502c3c64 |
parent 60754 | 02924903a6fd |
child 63161 | 2660ba498798 |
--- a/src/Doc/Codegen/Evaluation.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/Doc/Codegen/Evaluation.thy Tue Oct 06 15:14:28 2015 +0200 @@ -228,7 +228,7 @@ \<close> ML (*<*) \<open>\<close> -schematic_lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P" +schematic_goal "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P" ML_prf (*>*) \<open>val thm = Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*)