haftmann@37694: 
haftmann@37694: (* side-entry for HOL-Base *)
haftmann@37694: 
wenzelm@33615: use_thys ["HOL"];