clarified fulfill_norm_proof: no join_thms yet;
clarified priority of fulfill_proof_future, which is followed by explicit join_thms;
explicit Thm.future_body_of without join yet;
tuned Thm.future_result: join_promises without fulfill_norm_proof;
/* Title: Pure/Thy/thy_load.scala
Author: Makarius
Loading files that contribute to a theory.
*/
package isabelle
abstract class Thy_Load
{
def is_loaded(name: String): Boolean
def check_thy(dir: Path, name: String): (String, Thy_Header)
}