src/HOL/RealDef.thy
changeset 32657 5f13912245ff
parent 32069 6d28bbd33e2c
child 33197 de6285ebcc05
     1.1 --- a/src/HOL/RealDef.thy	Wed Sep 23 13:42:53 2009 +0200
     1.2 +++ b/src/HOL/RealDef.thy	Wed Sep 23 14:00:12 2009 +0200
     1.3 @@ -1128,8 +1128,8 @@
     1.4    by (simp add: of_rat_divide)
     1.5  
     1.6  definition (in term_syntax)
     1.7 -  valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
     1.8 -  [code_unfold]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
     1.9 +  valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
    1.10 +  [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"
    1.11  
    1.12  notation fcomp (infixl "o>" 60)
    1.13  notation scomp (infixl "o\<rightarrow>" 60)