equal
deleted
inserted
replaced
65 end; |
65 end; |
66 \<close> |
66 \<close> |
67 |
67 |
68 subsection \<open>evaluations functions\<close> |
68 subsection \<open>evaluations functions\<close> |
69 ML \<open> |
69 ML \<open> |
70 fun eval_is_ratequation_in _ _ (p as (Const ("RatEq.is_ratequation_in",_) $ t $ v)) _ = |
70 fun eval_is_ratequation_in _ _ (p as (Const (\<^const_name>\<open>RatEq.is_ratequation_in\<close>, _) $ t $ v)) _ = |
71 if is_rateqation_in t v |
71 if is_rateqation_in t v |
72 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) |
72 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) |
73 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) |
73 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) |
74 | eval_is_ratequation_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE); |
74 | eval_is_ratequation_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE); |
75 \<close> |
75 \<close> |