Lines Matching defs:fstr
511 val fstr = case f of
514 val restore_this = hide fstr
515 fun restore() = Parse.update_overload_maps fstr restore_this
521 val f_t = mk_var(fstr, type_of f_t0)
524 val fvs = List.filter (fn v => #1 (dest_var v) <> fstr) (free_vars c)
552 new_specification (fstr^"_def", [fstr], base_definition)
553 val _ = add_const fstr
554 val f_const = prim_mk_const {Name = fstr, Thy = current_theory()}
555 val f_thm = save_thm(fstr^"_thm",
569 val nm = fstr^"_equivariant"