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