src/Doc/Codegen/Evaluation.thy
changeset 59334 f0141b991c8f
parent 58620 7435b6a3f72e
child 59335 e743ce816cf6
     1.1 --- a/src/Doc/Codegen/Evaluation.thy	Fri Jan 09 21:20:07 2015 +0100
     1.2 +++ b/src/Doc/Codegen/Evaluation.thy	Sat Jan 10 10:24:30 2015 +0100
     1.3 @@ -326,7 +326,7 @@
     1.4    functions Fract
     1.5      "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
     1.6      "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
     1.7 -  file "examples/rat.ML"
     1.8 +  file "$ISABELLE_TMP/examples/rat.ML"
     1.9  
    1.10  text {*
    1.11    \noindent This merely generates the referenced code to the given