equal
deleted
inserted
replaced
425 else raise TEST lthy4 |
425 else raise TEST lthy4 |
426 |
426 |
427 |
427 |
428 val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms)) |
428 val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms)) |
429 val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms)) |
429 val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms)) |
|
430 val _ = tracing ("alpha_trans\n" ^ |
|
431 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_trans_thms)) |
430 |
432 |
431 val _ = |
433 val _ = |
432 if get_STEPS lthy > 11 |
434 if get_STEPS lthy > 11 |
433 then true else raise TEST lthy4 |
435 then true else raise TEST lthy4 |
434 |
436 |