equal
deleted
inserted
replaced
171 (** evaluation of numerals and predicates **) |
171 (** evaluation of numerals and predicates **) |
172 |
172 |
173 (*does a term contain a root ?*) |
173 (*does a term contain a root ?*) |
174 fun eval_root_free (thmid:string) _ (t as (Const(op0,t0) $ arg)) thy = |
174 fun eval_root_free (thmid:string) _ (t as (Const(op0,t0) $ arg)) thy = |
175 if strip_thy op0 <> "is'_root'_free" |
175 if strip_thy op0 <> "is'_root'_free" |
176 then raise error ("eval_root_free: wrong "^op0) |
176 then error ("eval_root_free: wrong "^op0) |
177 else if const_in (strip_thy op0) arg |
177 else if const_in (strip_thy op0) arg |
178 then SOME (mk_thmid thmid "" |
178 then SOME (mk_thmid thmid "" |
179 ((Syntax.string_of_term (thy2ctxt thy)) arg) "", |
179 ((Syntax.string_of_term (thy2ctxt thy)) arg) "", |
180 Trueprop $ (mk_equality (t, false_as_term))) |
180 Trueprop $ (mk_equality (t, false_as_term))) |
181 else SOME (mk_thmid thmid "" |
181 else SOME (mk_thmid thmid "" |