use_thy "WellForm"; (*The dynamic part of Bali, including type-safety*) use_thy "Evaln"; use_thy "Example"; use_thy "TypeSafe"; (*###use_thy "Trans";*) (*The Hoare logic for Bali*) use_thy "AxExample"; use_thy "AxSound"; use_thy "AxCompl";