Certain abstractions can be designated as soft. Some tactics treat soft abstractions as being transparent --- those tactics behave as if all soft abstractions had first been unfolded. In practice, those tactics only unfold soft abstractions when they need to and for the most part are careful not to leave unfolded soft abstractions in the subgoals that they generate.
Specific tactics and functions which unfold soft abstractions are:
where t is
soft and no well formedness lemmas exist for t, then it unfolds t.
In the basic libraries, the soft abstractions are
The logic abstractions ( and, or, implies, exists, all) are made soft because the well formedness rule for the underlying primitive term is simpler and more efficient than the well formedness lemma would be. The softness is also useful when one wishes to blurr the distinction between propositions and types, for example when reasoning explicitly about the inhabitants of propositions. member, nequal, rev_implies, ge and gt are soft principally because it can simplify matching.
Abstractions are not soft by default. They are declared soft by supplying their opids to the function add_soft_abs : tok list -> unit. Instances of this function are usually kept in ML objects in close proximity to the abstraction definitions that they are declaring soft. For an example use of add_soft_abs, see the object soft_ab_decls in the core_2 theory.