equal
deleted
inserted
replaced
84 use_thy "List"; |
84 use_thy "List"; |
85 |
85 |
86 init_pps (); |
86 init_pps (); |
87 print_depth 8; |
87 print_depth 8; |
88 |
88 |
89 val CHOL_build_completed = (); (*indicate successful build*) |
89 val HOL_build_completed = (); (*indicate successful build*) |