1 with_path ".." use_thy "HOL4Compat";
2 with_path ".." use_thy "HOL4Syntax";
3 setmp quick_and_dirty true use_thy "HOL4Prob";
4 setmp quick_and_dirty true use_thy "HOL4";