src/HOL/Decision_Procs/MIR.thy
changeset 45740 132a3e1c0fe5
parent 44890 22f665a2e91c
child 46130 4821af078cd6
     1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Fri Dec 02 14:37:25 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Fri Dec 02 14:54:25 2011 +0100
     1.3 @@ -5602,8 +5602,8 @@
     1.4    | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t))
     1.5    | term_of_num vs (@{code CF} (c, t, s)) = term_of_num vs (@{code Add} (@{code Mul} (c, @{code Floor} t), s));
     1.6  
     1.7 -fun term_of_fm vs @{code T} = HOLogic.true_const 
     1.8 -  | term_of_fm vs @{code F} = HOLogic.false_const
     1.9 +fun term_of_fm vs @{code T} = @{term True} 
    1.10 +  | term_of_fm vs @{code F} = @{term False}
    1.11    | term_of_fm vs (@{code Lt} t) =
    1.12        @{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::real"}
    1.13    | term_of_fm vs (@{code Le} t) =